Vous rejoindrez notre groupe LSL/CLASS, spécialisé en analyse sémantique de code source pour la sûreté et la sécurité des logiciels.

Plus précisément, vous rejoindrez l’équipe Frama-C, une plateforme open-source d’analyses formelles pour C, C++ ou JavaCard. Cette plateforme repose sur des techniques d’analyses avancées comme l’interprétation abstraite ou la vérification déductive. Elle est utilisée dans le monde académique mais aussi industriel que ce soit à des fins de sûreté de fonctionnement ou de sécurité, pour prévenir différentes vulnérabilités logicielles ou pour prouver des propriétés fonctionnelles ou de sécurité sur des codes de tailles variées.

Un des objectifs principaux de ce poste est de participer au développement et étendre les fonctionnalités des greffons les plus utilisés de Frama-C à savoir ceux basés sur des analyses formelles du code source.

Vos responsabilités seront les suivantes : 

·         Participer au développement de greffons existants mais aussi développer de nouvelles fonctionnalités et améliorations pour Frama-C

·         Interaction avec les utilisateurs et la communauté open-source

·         Valider les développements par l’analyse de cas d’études internes au laboratoire ou de certains de nos partenaires.

·         Contribuer à la communication des résultats scientifiques ou techniques de l’équipe

Vous êtes : 

- Titulaire d'un doctorat ou avez plus de trois ans d’expérience dans une équipe de recherche

- Maitrisez un langage fonctionnel (idéalement OCaml)

- Maitrisez finement les méthodes formelles (vérification déductive ou interprétation abstraite)

- Avez connaissance du langage C et la capacité à vous approprier d’autres langages

Sens du travail en équipe, capacité à la prise d’initiative et de responsabilité (encadrement et gestion de projet) appréciés