Post-doctoral researchers wanted for Coq Developments

by David Monniaux, July 7, 2018

VERIMAG has TWO open post-doc positions on Coq developments (certified distributed algorithms; certified compiler)

- Contracts: for 12 months
- Location: Grenoble, France
- Hosting institution: VERIMAG laboratory (Université Grenoble Alpes, CNRS Grenoble Institute of Technology)
- Scientific advisors: 1) Karine Altisen, Pierre Corbineau, Stéphane Devismes
2) Sylvain Boulmé, David Monniaux

How to Apply & Contact Information

Please send information requests/applications to
[email protected]
[email protected]
[email protected]
[email protected]
[email protected]

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 1) Distributed Algorithms or 2) Compiler Internals 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 one on distributed algorithms and one on certified compilers.

1) 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).

2) The CompCert compiler ( is proved to compile C programs while preserving their semantics. Each transformation or optimization phase comes with a proof of preservation of semantics. It has backends for various processors, including RiscV. VERIMAG is to develop and prove correct a backend for a secure variant of RiscV, in collaboration with the developers of that processor.