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:

a Master internship for Spring and Summer 2020, followed by a 3-years Ph.D.: Automatic Theorem Proving in Coq
a 2-years postdoc position: Automatic Theorem Proving in Coq and Application to Blockchains Verification
a 2-years research engineer position: Automatic Theorem Proving in Coq

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 13^th 2019