TRADUCTEUR SMT2.7 POUR L’ATELIER B

L’Atelier B consiste en un ensemble d’outils permettant la mise en œuvre de la méthode B, une méthode de développement logiciel basée sur les méthodes formelles. Elle est basée sur la preuve mathématique qu’une implémentation logicielle correspond à sa spécification, exprimée dans un langage formel. L’Atelier B est formé d’un cœur, ensemble d’outils assurant les activités liées à la preuve logicielle, et d’interfaces humain-machine, permettant d’orchestrer les outils du cœur.

Objectif du stage : Dans le cadre de sa démarche qualité logicielle, CLEARSY cherche à perfectionner son traducteur pog2smtlib-2.7 permettant d’utiliser des solveurs SMT dans le but d’améliorer l’automatisation des preuves dans Atelier B.

URL : https://github.com/CLEARSY/pog2smtlib-2.7

Livrables attendus :

• Documentation
• Nouvelle version de pog2smtlib-2.7

Compétences recherchées :

• Langage C++
• Logique mathématique
• Rigueur, autonomie, force de propositions