Distributed systems vary from peer-to-peer networks to distributed data bases or aircraft control systems. Fault tolerance means that the system will continue to respond even if one or several of the servers it is running on crashes, or if the network is congested, unreliable.
The internship focuses on the correctness of fundamental fault-tolerant distributed algorithms like consensus, in the benign (messages are lost, processes crash) and byzantine case (messages are corrupted). In the group, we have developed a domain specific programming language, called Psync, with a syntax and semantics that facilitates the implementation and the static analysis of fault-tolerant systems. Static analysis is an automated verification technique.
Given a specification (a set of properties) static analysis decides at compile time if the program satisfies the specification. The internship focuses on the development of several parts of the verification engine.
The applicant is encouraged to have one of the following:
- Good programming skills: C, Go, Python, Scala.
- Notions of program semantics
- Algorithms correctness proofs skills, logics (first-order, transitive closure).
We are looking for motivated candidates, that want to learn fast and contribute to the development of new verification methods. Knowledge about formal verification is not required, it will be accumulated during the internship.
The internship offers a glance into research, which means the main desired qualities of an intern are curiosity and perseverance.
The internship takes place at ENS, Ecole Normal Superieure, in Paris, 45 rue d’Ulm and is funded by INRIA, the french national institute for computer science. The intern will integrate the ENS/INRIA team Antique. The team has long standing history in fundamental research successfully transferred to the industrial world. The interns are supervised by Cezara Dragoi, CR INRIA, responsible for the distributed systems axe in the group.
The duration of the internship is 3 months.