Abstract interpretation for distributed system (Antique, Cezara Drăgoi) — sujet déjà choisi
Abstract interpretation is an analysis technique that can be used for automated verification.
For sequential programs, the automated verification problem made significant progress, either by using abstract interpretation or using other techniques: satisfiability solvers, model checking, etc.
For distributed systems, automatic verification is still in its early stages, despite massive usage of cloud technologies or distributed databases. The internship’s goal is to define abstract interpretation techniques that enable the automated verification of replicated state machine. Replicate state machine forms a subclass of distributed systems which ensure the coherences between independent copies of an application, which run over a network whose topology varies (ring, tree, dynamic dags, etc) and different types of failure may happen (process crash, message loss or corruption).
The project requires basic knowledge in programming languages. Notions in abstract interpretation and/or distributed systems are a plus but not mandatory. The project is in French or English.
Contact : Cezara Drăgoi