Une sémantique de flots dans Coq pour les structures de contrôle
Type de contrat : CDD
Niveau de diplôme exigé : Bac + 5 ou équivalent
Fonction : Ingénieur scientifique contractuel
Niveau d'expérience souhaité : Jeune diplômé
Contexte et atouts du poste
Contexte et atouts du poste
Le « Model-Based Design » est une approche moderne pour le développement de logiciels embarqués. L’idée est que les dessins dits schémas-blocs, que les ingénieurs utilisent pour modéliser un système et son environnement, peut être des spécifications précises et exécutables. De plus, il est même possible de transformer des parties vers du code de bas niveau pour une cible donnée. Dans le projet Vélus, nous nous donnons comme ambition de formaliser un langage de schémas-blocs et ses algorithmes de compilation dans un assistant de preuve, et de démontrer par preuve formelle que ces derniers préservent la sémantique du langage source jusqu’au code généré.
Principales activités
Travailler en équipe pour bien comprendre la problématique et se mettre d’accord sur les modèles sémantiques et les modifications requises au compilateur. En utilisant l’assistant de preuve Coq, ajouter de nouvelles fonctionnalités au compilateur prototype de Vélus et mettre à jour les preuves formelles.
Mission confiée
Le compilateur Vélus est développé dans l’équipe Inria PARKAS depuis quelques années. Nous avons étendu progressivement le langage source pour enlever la restriction aux programmes normalisés (Bourke et al. 2021) et ajouter les machines à états (Bourke, Pesin, and Pouzet 2023). Dernièrement, dans le travail de thèse de P. Jeanmaire, nous avons développé une sémantique dénotationnelle pour un sous-ensemble du langage (Bourke, Jeanmaire, and Pouzet 2022) dans le but de prendre en compte les erreurs arithmétiques, comme la division par zéro, venant du modèle sous-jacent fourni par CompCert (Leroy 2009), et de faciliter la vérification interactive des programmes.
Il s’agit maintenant d’étendre le travail de thèse de P. Jeanmaire en traitant les structures de contrôle, telles que la réinitialisation et le choix conditionnel sur les blocs d’équations et les machines à états, tout en développant le lien avec une sémantique à la Kahn dans l’assistant de preuve Coq.
Notre sémantique dénotationnelle est basée sur la bibliothèque de C. Paulin-Mohring (Paulin-Mohring 2009). Cette bibliothèque permet de formaliser les fonctions, les flots et les environnements comme de plus petits points fixes dans un ordre partiel complet. Nous nous en sommes servi pour définir la sémantique synchrone, c’est-à-dire, avec d’absences explicites, d’un sous-ensemble du langage d’entrée du compilateur Vélus. Nous avons démontré que, s’il y n’a pas d’erreur arithmétique, cette sémantique satisfait les prédicats de la sémantique relationnelle qui sert de spécification dans la preuve de correction du compilateur. Le premier but est d’étendre ce travail aux constructions syntaxiques définies sur les blocs d’équations. On commencera en traitant les variables locales en utilisant un point fixe sur les environnements qui associent des variables aux flots. Ensuite, on adaptera cette idée aux constructions de merge
, case
, reset
, et enfin les machines à états. Il faudra rétablir les propriétés clés sur le typage, le typage d’horloge, la causalité et le traitement d’erreurs arithmétiques.
Avec ses absences explicites, la sémantique synchrone donne une spécification du schéma de compilation (Biernacki et al. 2008). Une valeur n’est calculée et ne peut être utilisée que quand elle est présente. Par contre, pour la vérification interactive des programmes, les absences ne sont pas utiles (Canovas-Dumas and Caspi 2000), en plus, les définitions des opérateurs synchrones, ayant plus de cas, sont plus pénibles à manipuler dans un assistant de preuve. La solution est donc de définir une sémantique à la Kahn et de raisonner là-dedans. Les opérateurs de base sont déjà formalisés (Paulin-Mohring 2009), mais le lien avec la sémantique synchrone n’a pas été démontré dans Coq. Le second but est d’obtenir ce résultat. Il faudrait prendre en compte la possibilité d’erreurs arithmétiques et assurer le transfert des propriétés du modèle à la chaîne de compilation vérifiée existante. Les constructions sur les blocs d’équations seront traitées ou non selon la progression du travail.
Principales activités
Travailler en équipe pour bien comprendre la problématique et se mettre d’accord sur les modèles sémantiques et les modifications requises au compilateur. En utilisant l’assistant de preuve Coq, ajouter de nouvelles fonctionnalités au compilateur prototype de Vélus et mettre à jour les preuves formelles.
Compétences
-
Une formation solide dans la conception de langages de programmation. (requis)
-
Expérience de la programmation fonctionnelle. (souhaité)
-
Expérience de la modélisation et vérification formelle avec un assistant de preuve (Coq, HOL, PVS, Isabelle, Lean, etc.). (souhaité)
-
Expérience préalable de la programmation synchrone. (optional)
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
Informations générales
- Thème/Domaine :
Preuves et vérification
Ingénierie logicielle (BAP E) - Ville : Paris
- Centre Inria : Centre Inria de Paris
- Date de prise de fonction souhaitée : 2024-08-01
- Durée de contrat : 3 mois
- Date limite pour postuler : 2024-07-31
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : PARKAS
-
Recruteur :
Bourke Timothy / Timothy.Bourke@inria.fr
L'essentiel pour réussir
Une forte motivation pour appliquer la théorie des langages de programmation et de la logique formelle à la conception et l’amélioration de systèmes pratiques. La volonté de discuter et de collaborer de manière constructive avec d’autres chercheurs.
A propos d'Inria
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.