Doctorat
Equipe :
Renforcement du noyau d'un démonstrateur SMT : conception et implantation de procédures de décision efficaces
Début le 01/10/2009
Direction : CONCHON, Sylvain
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI / INRIA-SACLAY
Soutenue le 10/06/2013 devant le jury composé de :
M. Frédéric Besson - Examinateur
M. Sylvain Conchon - Encadrant, directeur de thèse
Mme Evelyne Contejean - Co-encadrante
M. Florent Hivert - Examinateur
M. Michaël Rusinowitch - Rapporteur
M. Ralf Treinen - Examinateur
Activités de recherche :
- Démonstration automatique, SMT et applications
Résumé :
Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.
Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.
L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire de Shostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT.
