Sciweavers

CAV
2007
Springer

A Tutorial on Satisfiability Modulo Theories

13 years 7 months ago
A Tutorial on Satisfiability Modulo Theories
Abstract. Solvers for satisfiability modulo theories (SMT) check the satisfiability of first-order formulas containing operations from various theories such as the Booleans, bit-vectors, arithmetic, arrays, and recursive datatypes. SMT solvers are extensions of Boolean satisfiability solvers (SAT solvers) that check the satisfiability of formulas built from Boolean variables and operations. SMT solvers have a wide range of applications in hardware and software verification, extended static checking, constraint solving, planning, scheduling, test case generation, and computer security. We briefly survey the theory of SAT and SMT solving, and present some of the key algorithms in the form of pseudocode. This tutorial presentation is primarily directed at those who wish to build satisfiability solvers or to use existing solvers more effectively.
Leonardo Mendonça de Moura, Bruno Dutertre,
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where CAV
Authors Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar
Comments (0)