Ingénieur Recherche et Développement (H/F), Vérification formelle de programmes Rust

Le centre de recherche Inria de Saclay a été créé en 2008. Sa dynamique s’inscrit dans le développement du plateau de Saclay, en partenariat étroit d’une part avec le pôle de l’Université Paris-Saclay et d’autre part avec le pôle de l’Institut Polytechnique de Paris . Afin de construire une politique de site ambitieuse, le centre Inria de Saclay a signé en 2021 des accords stratégiques avec ces deux partenaires territoriaux privilégiés.

Le centre compte 39 équipes-projets , dont 27 sont communes avec l’Université Paris-Saclay ou l’Institut Polytechnique de Paris. Son action mobilise plus de 600 personnes , scientifiques et personnels d’appui à la recherche et à l’innovation, issues de 54 nationalités.

Le centre Inria Saclay - Île-de-France est un acteur essentiel de la recherche en sciences du numérique sur le plateau de Saclay. Il porte les valeurs et les projets qui font l’originalité d’Inria dans le paysage de la recherche : l’excellence scientifique, le transfert technologique, les partenariats pluridisciplinaires avec des établissements aux compétences complémentaires aux nôtres, afin de maximiser l’impact scientifique, économique et sociétal d’Inria.

Ce poste est proposé dans le cadre du projet Décysif
(https://decysif.fr/), un projet collaboratif qui vise à appliquer des
méthodes formelles pour apporter des garanties de correction des programmes
critiques pour la sureté et la sécurité. Ce projet réunit l'équipe
Inria Toccata (https://toccata.gitlabpages.inria.fr/toccata/) et des
partenaires industriels dont les sièges sont à Paris: TrustInSoft,
AdaCore et OCamlPro. L’objectif général est de contribuer aux
activités de vérification formelle chez tous partenaires, autour de la
vérification des programmes en Ada, C, C++ et Rust, avec des
techniques faisant appel aux outils de preuve développés par l'équipe
Toccata, en particulier Why3.

Les travaux seront effectués en majorité dans les locaux de l'équipe
Toccata à Gif-sur-Yvette, mais également en partie dans les locaux des
sociétés partenaires à Paris. les frais de déplacements seront pris en
charge dans la limite du barème en vigueur.

En collaboration directe avec les développeurs de Why3 chez Toccata et
avec les ingénieurs-chercheurs chez les partenaires, la personne
recrutée devra travailler à la maturation du prototype Creusot
(https://github.com/xldenis/creusot) dédié à la preuve de programmes
Rust. Ce prototype est issu d'une thèse de doctorat et devra être
amélioré pour pouvoir être appliqué à des cas d'études d'origine
industrielle. Les objectifs concernent entre autres l'élargissement du
fragment de Rust supporté, le besoin de compléter les spécifications
des bibliothèques, d'améliorer l'utilisabilité de l'interface
graphique, d'augmenter du taux d'automatisation des preuves, de mettre
en place des aides à la preuve (comme la génération de contre-exemples
pertinents en cas d'échec de la preuve), de renforcer la robustesse et la
reproductibilité des preuves.

Développement logiciel en Rust et en OCaml, développement de
spécifications de bibliothèques en Why3 et en Rust, utilisation de
solveurs SMT externes, expérimentations logicielles, écriture de
documentation, contribution à la rédaction d'articles scientifiques.

On recherche des candidats possédant le plus d'expérience et de
compétences possibles parmi : le développement avec le langage OCaml ;
le développement avec le langage Rust ; les techniques d'évaluation,
de compilation et/ou de transformation de programmes ; les méthodes
formelles de développement logiciel ; les logiques formelles ;
l'analyse statique de programmes ; la preuve assistée par ordinateur ;
l'utilisation d'environnements de preuve formelle.

Un niveau d'anglais au moins à l'écrit est exigé. A l'oral l'anglais
ou le français devra être suffisamment maîtrisé.

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale

Rémunération en fonction de l'expérience professionelle