Informations générales
Entité de rattachement
Le Commissariat à l'énergie atomique et aux énergies alternatives (CEA) est un organisme public de recherche.
Acteur majeur de la recherche, du développement et de l'innovation, le CEA intervient dans le cadre de ses quatre missions :
. la défense et la sécurité
. l'énergie nucléaire (fission et fusion)
. la recherche technologique pour l'industrie
. la recherche fondamentale (sciences de la matière et sciences de la vie).
Avec ses 16000 salariés -techniciens, ingénieurs, chercheurs, et personnel en soutien à la recherche- le CEA participe à de nombreux projets de collaboration aux côtés de ses partenaires académiques et industriels.
Référence
2023-26280
Description de l'unité
Au sein du Département Ingénierie Logiciels et Systèmes (DILS), le Laboratoire pour la Sûreté et Sécurité des Logiciels (LSL) œuvre au développement et au transfert industriel de différentes technologies de vérification formelle d'analyse de programmes, pour en assurer de très hauts degrés de sûreté et/ou de sécurité.
Description du poste
Domaine
Mathématiques, information scientifique, logiciel
Contrat
CDD
Intitulé de l'offre
Ingénieur-Chercheur en méthodes formelles et analyse de code source H/F
Statut du poste
Cadre
Durée du contrat (en mois)
36
Description de l'offre
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 une base commune dédiée à la modélisation du langage d’entrée, et utilisée par diverses analyses formelles. 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 du noyau de Frama-C, notamment en vue d’améliorer sa capacité à passer à l’échelle sur des systèmes toujours plus grands.
Responsabilités
· Participer au développement du noyau de Frama-C mais aussi adapter les greffons existants à ces modifications
· 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
Profil du candidat
· Doctorat ou plus de trois ans d’expérience dans une équipe de recherche
· Maitriser un langage fonctionnel (idéalement OCaml)
· Maitrise en méthodes formelles ou sémantique de langages
· Connaissance du langage C et capacité à s’approprier d’autres langages
Sens du travail en équipe, capacité à la prise d’initiative et de responsabilité (encadrement et gestion de projet)
Localisation du poste
Site
Saclay
Localisation du poste
France
Ville
Palaiseau
Demandeur
Disponibilité du poste
01/04/2023
Je me crée un espace candidat
