ANR a sélectionné le projet BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) dans la cadre de l’appel à projets générique 2020.
- DURÉE : 48 mois
- PARTENAIRES: INRIA Nancy (leader), CLEARSY, CRIL Lens, Université de Liège
Le projet BLaSST vise à établir un pont entre des techniques combinatoires et symboliques en déduction automatique en vue de résoudre des obligations de preuves issues de modèles B.
Les travaux contribuent à avancer l’état de l’art en déduction automatique, notamment les techniques SAT et SMT, et à rendre ces techniques plus largement disponibles pour la vérification de logiciels.