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