PhD offer at Inria Rennes, France

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 cyber and physical aspects of such designs. Our approach is based on
components augmented with formal contracts that can be composed,
abstracted or refined. It focuses on automating proofs of system-level
properties and requirements from individual proofs of component properties
(with, e.g., theorem provers, static analysers). This approach should be
semantically grounded, 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 information:

Comments are closed.