(repost from the mailing list firstname.lastname@example.org)
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
spe######ts) 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 athttps://jobs.inria.fr/public/classic/fr/offres/2019-01424