Augmenter les outils de raisonnement sur le langage B par des techniques SAT et SMT – BLaSST

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. Plus concrètement, des encodages, d'optimisations des techniques de résolution ainsi que la construction de modèles et la suggestion de lemmes seront considérés. En recombinant ces avancées, l'impact scientifique attendu est (i) 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 et (ii) des retours utiles en cas de conditions de vérification qui ne peuvent être démontrées correctes. 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.