INFERENCE DE TYPES APPLIQUEE AU LANGAGE B
Inférence de types appliquée au langage B
Objectif : Moderniser et améliorer le traitement des types dans Atelier B, par intégration de l’inférence de types dans les outils d’analyse des sources et de génération d’obligation de preuve de l’Atelier B
Contexte :
Atelier B est un environnement de développement pour le langage B. Il permet de spécifier, de développer et de vérifier des logiciels critiques. Il est notamment utilisé pour la certification critères communs de cartes à puce ainsi que dans le domaine ferroviaire. Atelier B représente les composants analysés sous la forme de fichiers ainsi que les obligations de preuve dans des formats XML. Les informations de typage des expressions générées par l’analyseur sont issues d’un algorithme de vérification des types qui ne permet pas de typer de manière satisfaisante toutes les expressions, et qui impose des contraintes importantes sur la rédaction des sources (tout identifiant doit avoir été typé avant d’être utilisé). On souhaite donc remplacer cet algorithme par un algorithme d’inférence de types qui permettra de typer toutes les expressions, et qui permettra de lever les contraintes de rédaction des sources. L’outil atypik est un prototype développé par CLEARSY qui effectue la phase d’inférence de types sur les fichiers XML en utilisant un solveur SMT pour résoudre les contraintes.
Le stage est structuré comme suit
- Développer un composant de résolution de contraintes de typage pour remplacer le composant sur étagère généraliste actuellement utilisé sur la base de l’article “An Abstract Decision Procedure for a Theory of Inductive Data Types” (Barrett, Shikanian et Tinelli)
- Mettre en place le composant d’inférence de types au sein de l’analyseur de sources (https://github.com/CLEARSY/BCOMPILER).
En cas de complétion rapide de ces tâches, les tâches suivantes pourront être réalisées :
- Adapter le générateur d’obligations de preuve aux informations de typage enrichies.
- Utiliser le moteur d’inférence de types dans le prouveur interactif pour permettre l’appel à des prouveurs externes.
- Adapter le transcodeur Rust pour tirer partie des informations de typage enrichiers.
- Améliorer le traducteur POG vers TPTP pour prendre en compte les nouvelles informations de typage.
- Améliorer le traducteur POG vers SMT pour prendre en compte les nouvelles informations de typage.
- Améliorer le traducteur POG vers WhyML pour prendre en compte les nouvelles informations de typage.
Compétences recherchées :
- Goût pour la recherche d’algorithmes et de structures de données efficaces
- Solides connaissances de C++
- Gestion de configuration avec Git
-
Localisation : Aix-Paris
Durée : 6 mois
Niveau : Bac +5
Pour postuler merci d’envoyer un Cv et une Lettre de motivation à l’adresse :