Description : Interopérabilité pour les preuves et les programmes / Interoperability for Proofs and Pro-
grams

Les méthodes formelles regroupent aujourd’hui de nombreux outils de spécification, de modélisation, d’analyse statique et dynamique pour démontrer des propriétés mathématiques et établir la correction de programmes informatiques. Si l’on est aujourd’hui en capacité d’utiliser chacun de ces outils individuellement pour des vérifications de taille conséquente, leur combinaison reste hors de portée de l’état de l’art. Ils reposent notamment sur des formalismes distincts et peuvent être spécialisés pour des objectifs spécifiques. L’objectif de ce défi est de faciliter l’interopérabilité entre les nombreux outils existants et ainsi d’améliorer l’expérience utilisateur lors des développements formels et de leur maintenance en intégrant ce domaine comme une partie usuelle du développement logiciel.