2020-02999 - Post-Doctoral Research Visit F/M Verified Abstract Machines for Operating Systems
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Contrat renouvelable : Oui

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

Contexte et atouts du poste

This project is funded by the ANR and involves a collaboration between the Inria teams Whisper and Antique, and the ERODS team at the University of Grenoble.


Mission confiée

Assignments :
The postdoc will contribute to the design and development of prrofs using tools such as Why3 of correctness properties of abstract machines for operating system services.  The project will furthermore involve consideration of how the designed proof strategies can facilitate memory-level verification with MemCAD.

Principales activités

Main activities (5 maximum) :

Design and devlopment of proofs of abstract machines.  Consideration of how MemCAD can be used to address the considered correctness issues.



Technical skills and level required : A strong background in the design and in the use of (semi)-automatic theorem proving tools is essential for this project.


  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage