The Coq mailing list

[Jean-Pierre Talpin <jean-pierre.talpin AT inria.fr>]

Applications are invited for a doctoral project on the elaboration of a logical framework to verify requirements of hybrid system models.

 

The goal of this project is to build cyber-physical systems with a correct-by-construction approach in order to verify requirements against both digital and physical aspects of such designs. Our approach is based on components augmented with formal contracts that are expressed using differential dynamic logic and can be composed, abstracted or refined. We focus on automating proofs of system-level properties and requirements from individual, possibly mechanized, proofs of component properties (with, e.g., theorem provers, static analyzers). The envisioned framework should, in the end, be usable by regular engineers (i.e. not proof theory specialists) and tooled.

 

The ideal candidate will have a strong background in logic, concurrency, proof, verification, and experience and interest in control theory and embedded system design.  The successful applicant will be employed by the Industrial partner of the project: Mitsubishi Electric R&D Centre Europe, under a three years CIFRE grant, and embedded with Inria project-team TEA at Inria, Rennes (Brittany, France). 

 

Detailed offer and complete information at https://jobs.inria.fr/public/classic/fr/offres/2019-01424