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

Télécharger l'offre au format PDF

Type de contrat : CDD

Contrat renouvelable : Oui

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

Autre diplôme apprécié : Thèse de doctorat en Informatique

Fonction : Ingénieur scientifique contractuel

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

A propos du centre ou de la direction fonctionnelle

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 40 équipes-projets , dont 32 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.

Contexte et atouts du poste


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.

Mission confiée


En collaboration directe avec les chercheurs 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.

Principales activités


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.

Compétences


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é.

Avantages

  • 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

Selon expérience professionnelle