VERIMAG has on open post-doc positions on Coq developments for distributed algorithms
- Contracts: for 12 months
- Location: Grenoble, France
- Hosting institution: VERIMAG laboratory (Université Grenoble Alpes, CNRS Grenoble Institute of Technology)
- Scientific advisors: Karine Altisen, Pierre Corbineau, Stéphane Devismes
How to Apply & Contact Information
Please send information requests/applications to Karine.Altisen@univ-grenoble-alpes.fr, Pierre.Corbineau@univ-grenoble-alpes.fr, Stephane.Devismes@univ-grenoble-alpes.fr
Email subject MUST start with "[Post-Doc Coq]"
Applications must include the following documents:
- Letter of application: why you are interested in this research position and what you would like to work on
- Curriculum vitae
- References or letters of recommendation
- Applicant’s scientific report or paper written in English
- Any other document showing that you are an outstanding candidate
Required Skills
- Software Development
- Theorem Proving (preferably with Coq)
- Knowledge in Distributed Algorithms is a plus
Coq is a proof assistant mixing software development in a purely functional strongly-typed language and theorem proving.
VERIMAG is a leading laboratory in methods for the development of safety-critical systems. There are several ongoing efforts at VERIMAG on Coq proofs, including on distributed algorithms.
Distributed systems must tolerate faults. Self-stabilization is a versatile lightweight technique to withstand transient faults in a distributed system. After transient faults hit and place the system into some arbitrary global state, a self-stabilizing algorithm returns, in finite time, to a correct behavior without external intervention. We are currently developing a framework called PADEC, based on Coq, to (semi-)automatically construct certified proofs of self-stabilizing algorithms. We import into Coq the computational model in which the targeted algorithm is designed, formalize the algorithm itself and then prove that it respects its specification (safety, convergence, and some performance criteria).
