BLANC - Programme non thématique - Appel à projets de recherche

Assister Automatiquement les Assistants de Preuve Avec des Traces – A3PAT

Résumé de soumission

Les assistants à la preuve comme COQ bénéficient d'un noyau de vérification très sûr mais souffrent d'un manque d'automatisation. Des outils de preuve automatique performants existent mais leurs réponses ne sont pas vérifiables mécaniquement. Parmi ceux-ci, CiME est l'un des tout meilleurs sur la scène internationale pour les problèmes liés à la récriture : terminaison, complétion, etc. Notre objectif est de permettre aux assistants de preuve d'interroger des prouveurs automatiques satellites tout en préservant le haut degré de confiance qu'on leur accorde. Nous envisageons de répondre à cette forte demande par la génération de certificats à partir de traces. Cet objectif nécessite une importante étude théorique et doit se matérialiser à terme en un outil. Une première étape fondamentale est la définition d'un langage de traces capable d'exprimer la diversité de preuves de propriétés aussi complexes que terminaison ou confluence. Cette définition s'accompagne d'une modélisation des propriétés souhaitées, notamment pour garantir la complétude de certaines procédures. Il faut ensuite étudier la génération de traces pour les procédures de décision récentes, en particulier celles qui sont mises en oeuvre dans le logiciel CiME 2, développé par certains membres de notre groupe. À terme les résultats prendront forme dans une nouvelle version de CiME capable de communiquer avec COQ.

Coordinateur du projet

CONSERVATOIRE NATIONAL DES ARTS ET METIERS (CNAM) (Laboratoire public)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

UNIVERSITE BORDEAUX I
INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE -(INRIA Centre Sophia-Antipolis)
CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR SUD
CONSERVATOIRE NATIONAL DES ARTS ET METIERS (CNAM)

Aide de l'ANR 234 999 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles