Dans le cadre d’un projet financé par l’Agence National de recherches (ANR), CLEARSY collabore avec le LORIA (Nancy), le CRIL (Lens) et l’Université de Liège pour améliorer les outils de démonstration mathématique de l’Atelier B.
Quand on utilise l’Atelier B pour réaliser des logiciels sécuritaires , celui-ci produit des obligations de preuves mathématiques qu’il faut ensuite résoudre.
Les outils de démonstration (prouveurs) de l’Atelier B permettent déjà d’en résoudre automatiquement une grande partie. Le projet « Enhancing B Language Reasoners with SAT and SMT Techniques” vise améliorer l’efficacité de ces démonstrateurs.
Les premiers résultats sont déjà concluants !
Sur un banc de tests de 681 285 obligations de preuves, les techniques basées sur des outils de vérification de cohérence de type SAT et de contrôle de cohérence de type SMT nous permettent de passer de 74% à 87% d’obligations de preuve prouvées automatiquement.
OBJECTIF : Plus de 90% à la fin du projet en mars 2027 !