Combining decision procedures by (model-)equality propagation

Abstract : Formal methods in software and hardware design often generate formulas that need to be validated, either interactively or automatically. Among the automatic tools, SMT (Satisfiability Modulo Theories) solvers are particularly suitable to discharge such proof obligations, since their input language is equational logic with symbols from various useful decidable fragments such as uninterpreted symbols, linear arithmetic, and usual data-structures like arrays or lists. In this paper, we present an approach to combine decision procedures and propositional solvers into an SMT-solver. This approach is based not only on the exchange of deducible equalities between decision procedures, but also on the generation of model equalities by decision procedures. This extends nicely the classical Nelson-Oppen combination procedure in a simple platform to smoothly combine convex and non-convex theories. We show the soundness and completeness of this approach using an original abstract framework to represent and reason about SMT-solvers. We then describe an algorithmic translation of this method, implemented in the kernel of the veriT solver.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2010, 240 (2 July 2009), pp.113-128. 〈10.1016/j.entcs.2009.05.048〉
Liste complète des métadonnées
Contributeur : Pascal Fontaine <>
Soumis le : lundi 6 décembre 2010 - 16:33:59
Dernière modification le : mardi 24 avril 2018 - 13:54:34

Lien texte intégral




Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Science of Computer Programming, Elsevier, 2010, 240 (2 July 2009), pp.113-128. 〈10.1016/j.entcs.2009.05.048〉. 〈inria-00543801〉



Consultations de la notice