Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Procédures de Décision Génériques pour des Théories Axiomatiques du Premier Ordre
Début le 17/12/2010
Direction : MARCHÉ, Claude
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI & Sté AdaCore
Soutenue le 01/04/2014 devant le jury composé de :
Directeurs de thèse :
Claude MARCHÉ (Directeur de Recherche à l'Inria Saclay–Île-de-France)
Andrei PASKEVICH (Maitre de Conférences à l'Université Paris-Sud)
Composition du jury :
Rapporteurs :
Nikolaj BJØRNER (Principal Researcher à Microsoft Research)
Albert RUBIO (Professeur à l'Universitat Politècnica de Catalunya)
Examinateurs :
Joffroy BEAUQUIER (Professeur à l'Université Paris-Sud) Stephan MERZ (Directeur de Recherche à l'Inria Nancy)
Invités :
Johannes KANIG (Ingénieur de Recherche à AdaCore)
Yannick MOY (Ingénieur de Recherche à AdaCore)
Activités de recherche :
- Démonstration automatique, SMT et applications
Résumé :
Les solveurs SMT sont des outils dédiés à la vérifications d'un ensemble de formules mathématiques, en général sans quantificateurs, utilisant un certain nombre de théories prédéfinies, telles que la congruence, l'arithmétique linéaire sur les entiers, les rationnels ou les réels, les tableaux de bits ou les tableaux. Ajouter une nouvelle théorie à un solveur SMT nécessite en général une connaissance assez profonde du fonctionnement interne du solveur, et, de ce fait, ne peut en général être exécutée que par ses développeurs.
Pour de nombreuses théories, il est également possible de fournir une axiomatisation finie en logique du premier ordre. Toutefois, si les solveurs SMT sont généralement complets et efficaces sur des problèmes sans quantificateurs, ils deviennent imprévisibles en logique du premier ordre. Par conséquent, cette approche ne peut pas être utilisée pour fournir une procédure de décision pour ces théories.
Dans cette thèse, nous proposons un cadre d'application permettant de résoudre ce problème en utilisant des déclencheurs. Les déclencheurs sont des annotations permettant de spécifier la forme des termes avec lesquels un quantificateur doit être instancié pour obtenir des instances utiles pour la preuve. Ces annotations sont utilisées par la majorité des solveurs SMT supportant les quantificateurs et font partie du format SMT-LIB v2.
Dans notre cadre d'application, l'utilisateur fournit une axiomatisation en logique du premier ordre de sa théorie, ainsi qu'une démonstration de sa correction, de sa complétude et de sa terminaison, et obtient en retour un solveur correct, complet et qui termine pour sa théorie. Dans cette thèse, nous décrivons comment un solveur SMT peut être étendu à notre cadre nous basant sur l'algorithme DPLL modulo théories, utilisé traditionnellement pour modéliser ls solveurs SMT. Nous prouvons également que notre extension a bien les propriétés attendues.
L'effort à fournir pour implémenter cette extension dans un solveur SMT existant ne doit être effectué qu'une fois et le mécanisme peut ensuite être utilisé sur de multiple théories axiomatisées. De plus, nous pensons que, en général, cette implémentation n'est pas plus compliquée que l'ajout d'une unique théorie au solveur. Nous avons fait ce travail pour le solveur SMT Alt-Ergo, nous en présentons certains détails dans la thèse.
Pour valider l'utilisabilité de notre cadre d'application, nous avons prouvé la complétude et la terminaison de plusieurs axiomatizations, dont une pour les listes impératives doublement chaînée, une pour les ensembles applicatifs et une pour les vecteurs de Ada. Nous avons ensuite utilisé notre implémentation dans Alt-Ergo pour discuter de l’efficacité de notre système dans différents cas.
