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: https://jobs.inria.fr/public/classic/fr/offres/2019-01424
Master of Science in Informatics at Grenoble (MOSIG 2016-2020)
