A Post-Doctoral position is available as part of the funded ANR project CoMeMoV (https://comemov.github.io) between the LIFO (https://www.univ-orleans.fr/lifo/) (University of Orleans, France), CEA List (Home page) and Thales Research and Technology (Research and Technology | Thales Group).
Frama-C (https://www.frama-c.com/) is an extensible and collaborative open-source platform dedicated to source-code analysis of C software. If offers a specification language and various analyzers in the form of separate plugins. The WP plugin of Frama-C can be used to prove that a given C program respects its specification. WP provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial-strength programs, this combination already makes WP mature enough to be deployed for proving critical industrial embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to allow deductive verification with WP to better scale on complex industrial programs.
The work of the successful candidate will mainly focus on the formalization and proof of correctness of the proposed collaborative memory models for deductive verification.
Application requirements:
-
PhD (obtained or to be obtained soon) in Computer Science
-
Technical background in formal methods, in particular, in interactive theorem proving (preferably with Coq)
-
Technical background in programming in C
-
Strong communication skills and teamwork capabilities
-
English language fluency in both speaking and writing
The position is available immediately, but can start later in Fall 2023. Applications will be considered until the position is filled.
This is a research-only position, for 21 months.
Please send the application materials or any questions to Frederic Loulergue (Frederic.Loulergue@univ-orleans.fr).
Best regards,
Frederic Loulergue
–
Professeur
Université d’Orléans
UFR Collegium Sciences & Techniques
Directeur des études du M1 Informatique
Laboratoire d’Informatique Fondamentale d’Orléans (LIFO)
Responsable de l’équipe LMV - Langages Modèles et Vérification
https://frederic.loulergue.eu