L’automatisation de la preuve et le support interactif à la preuve sont des éléments clés de l’application des méthodes formelles pour la conception de logiciels et de systèmes. Depuis plus de 20 ans, CLEARSY maintient et distribue des prouveurs de théorèmes automatiques et interactifs avec l’Atelier B, l’environnement graphique industriel de développement pour la méthode B et pour Event-B. La méthode B fournit un cadre formel pour le développement de composants logiciels critiques, tandis que Event-B est une notation formelle pour la conception et l’analyse de systèmes.
En complément à ces outils, CLEARSY poursuit des activités de R&D dans le domaine de la vérification formelle, en collaborant étroitement avec la communauté universitaire. De 2012 à 2016, CLEARSY a été partenaire du projet BWare, financé par l’ANR (Agence Nationale de la Recherche), qui a permis d’explorer l’application de la plateforme de vérification déductive de programmes Why3. Un résultat concret de Bware fut la mise en œuvre de « iapa », un nouveau composant dans l’Atelier B, qui permet à l’utilisateur, en utilisant Why3 comme passerelle, d’appliquer des prouveurs disponibles sur étagères pour traiter des obligations de preuve.
Dans le cadre du projet ANR DISCONT, démarré en 2017, CLEARSY a intégré à Atelier B deux nouvelles fonctionnalités pour améliorer le support de preuve. D’une part, des solveurs SMT peuvent être utilisés dans le prouveur interactif, pour essayer de prouver des sous-buts via la résolution SMT. D’autre part, ces mêmes solveurs SMT peuvent être appliqués directement aux obligations de preuve brutes grâce à un encodage de la logique B adapté à ces outils.
À partir de 2022, et grâce aux moyens mis à disposition par l’ANR, CLEARSY s’impliquera dans deux nouveaux projets de recherche collaborative sur le support à la preuve.
BLaSST vise à augmenter le taux de réussite de l’automatisation des preuves en améliorant l’encodage SMT ainsi qu’à explorer de nouveaux encodages, tels que SAT et pseudo-booléens, qui sont particulièrement adaptés à des tâches de vérification et à la réfutation automatiques. ICSPA développera lui un cadre théorique et pratique pour augmenter la confiance dans les outils de preuve, créant ainsi de nouvelles opportunités d’intégration de technologies de vérification formelle dans l’Atelier B.