ANR PRCE BLaSST
Enhancing B Language Reasoners with SAT and SMT Techniques
Les partenaires de ce projet sont INRIA Nancy (porteur), ULiège and Clearsy.
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 concernent des techniques propositionnelles ainsi que des formalismes SMT plus expressifs, en considérant des encodages, optimisations, construction de modèles et suggestion de lemmes. En recombinant ces avancées, l’impact scientifique attendu est un taux d’automatisation élevé grâce à des techniques de raisonnement en logique de l’ordre supérieur ainsi qu’à des techniques d’instanciation énumérative pour des domaines finis. L’efficacité des méthodes issues du projet sera quantifiée en les appliquant à des collections de problèmes fournies par le partenaire industriel. L’impact dans l’industrie sera une productivité accrue des ingénieurs de vérification. Les collections de problèmes et les outils de résolution seront mis à disposition publiquement, avec des licences open-source permissives.