Combining decision procedures by (model-)equality propagation

  • De Oliveira D
  • Déharbe D
  • Fontaine P
  • 5

    Readers

    Mendeley users who have this article in their library.
  • 1

    Citations

    Citations of this article.

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, as 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, 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 NelsonOppen 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 (Bouton et al. (2009)) [9]. © 2010 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Automated theorem proving
  • Combination of decision procedures
  • Formal verification
  • SMT solving

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free