Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Toccata

Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq

Début le 16/07/2007
Direction : CONTEJEAN, Evelyne

Ecole doctorale :
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : LRI-INRIA PROVAL

Soutenue le 04/01/2011 devant le jury composé de :
Rapporteurs
Pierre Crégut (Orange Labs)
Shankar Natarajan (SRI)

Examinateurs
Hugo Herbelin (INRIA)
Sava Krstic (Intel)
Burkhart Wolff (Paris-Sud)

Encadrants
Evelyne Contejean (CNRS)
Sylvain Conchon (Paris-Sud)

Activités de recherche :

Résumé :
Dans cette thèse, nous proposons une amélioration de l'automatisation
des preuves dans l'assistant de preuve Coq. Cette automatisation est
obtenue en intégrant à Coq les procédures de décision pour la logique
propositionnelle, l'égalité et l'arithmétique linéaire constituant le
noyau du solveur SMT Alt-Ergo. Cette intégration est réalisée en
utilisant la technique de preuve par réflexion, qui consiste à
développer en Coq ces algorithmes et à prouver formellement leur
correction de manière à les exécuter directement dans l'assistant de
preuve. Comme les algorithmes formalisés en Coq sont exactement ceux
utilisés dans le noyau d'Alt-Ergo, notre travail permet également
d'augmenter considérablement la confiance que l'on peut avoir dans ce
dernier. En particulier, il utilise un algorithme original de
combinaison de l'égalité modulo une théorie, inspiré de la combinaison
de Shostak et appelé CC(X), et dont la justification est relativement
complexe.

Notre développement Coq est utilisable sous la forme de
tactiques qui permettent de valider automatiquement des formules
combinant logique propositionnelle, égalité et arithmétique. Afin que
ces tactiques soient le plus efficaces possibles, nous avons attaché
une grande importance aux performances de notre implantation Coq, et
en particulier à l'utilisation de structures de données efficaces
courantes, dont nous proposons ici une bibliothèque.