PhD Position F/M Foundational Verification of Interactively Optimized Programs

Télécharger l'offre au format PDF
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

Niveau d'expérience souhaité : Jeune diplômé

Contexte et atouts du poste

Part of ANR-OptiTrust project.

Mission confiée

Producing formally verified code is a challenging, time-consuming task.
Producing highly optimized code is another challenging, time-consuming task.
The OptiTrust project aims at developing code that features both high performance
and formal verification.

The OptiTrust approach is based on interactive compilation, whereby the
programmer explicitly indicates what optimizations to apply and where to
apply them in the code. The key idea is to preserve formal invariants
throughout a sequence of source-to-source transformations.

The aim of the PhD is to provide foundational guarantees to the approach.

Principales activités


Concretely, we aim to ultimately produce Rocq proofs of correctness for the
code optimized using OptiTrust. We will investigate the following aspects.

1. Extend OptiTrust to make its internal language support high-level code,
   including non-executable specifications.

2. Formalize in Rocq the semantics of this extended internal language.

3. Develop an extraction from typed OptiTrust programs into proof terms
   in a standard separation logic, shallowly embedded in Rocq.

4. Develop a formally verified translation from OptiTrust's langage into
   the input language of a formally verified compiler such as CakeML.

Compétences

Concretely, the candidate will contribute to the design of the framework,
its implementation in OCaml, to the development of the case studies, but
also to the writing and presentation of research papers on the work produced.

The candidate must have a strong experience in a functional language, ideally OCaml.
experience in programming and basic notions of program optimization.
In addition, the candidate must have a Master in computer sciences, focused
covering topics of the semantics and typechecking of programming languages,
and have good english skills.

Avantages

  • 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

Rémunération

2200 € brut/mois