Research positions

We are looking for a PhD student, a 2-years postdoc and a 2-years research engineer to work on automatic theorem proving in Coq and its application to blockchain verification.

The first objective is the development of SMTCoq, a plugin to safely enjoy automatic theorem proving inside Coq. In collaboration with the Nomadic Labs company, a second objective is the application of proof automation to the verification of the Tezos blockchain.

The detailed research positions are:
The recruited persons will be part of Universite Paris-Saclay, and a member of the Inria team Deducteam.

Contact me if interested!

Last update: November 13th 2019