Skip to Main content Skip to Navigation
New interface
Conference papers

Combining decision procedures by (model-)equality propagation

Diego Caminha B. de Oliveira 1 David Déharbe 2 Pascal Fontaine 1 
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : SMT (Satisfiability Modulo Theories) solvers are automatic verification engines suitable to discharge important classes of proof obligations generated in applying formal construction of software and hardware designs. In this paper, we present a new approach to combine decision procedures and propositional solvers into an SMT-solver. This approach is based on the generation of model equalities by decision procedures. We show the soundness and completeness of the proposed approach using an original abstract framework to represent and reason about SMT-solvers. We then present an algorithmic version of the new SMT-solving approach and discuss practical aspects of our implementation.
Document type :
Conference papers
Complete list of metadata
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Monday, November 10, 2008 - 1:04:09 PM
Last modification on : Friday, February 4, 2022 - 3:31:28 AM


  • HAL Id : inria-00337979, version 1



Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Brazilian Symposium on Formal Methods - SBMF 2008, Aug 2008, Salvador, Bahia, Brazil. ⟨inria-00337979⟩



Record views