Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

Ph.D
Group :

Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures

Starts on 01/10/2009
Advisor : CONCHON, Sylvain

Funding :
Affiliation : Université Paris-Saclay
Laboratory : LRI / INRIA-SACLAY

Defended on 10/06/2013, committee :
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

Research activities :
   - Automated Proof, SMT and Applications

Abstract :
This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.

SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.

This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutative symbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.