Satisfiability and Theories

Author

Voronkov, Andrei

Author_Institution

Univ. of Manchester, Manchester, UK

fYear

2009

fDate

26-29 Sept. 2009

Firstpage

16

Lastpage

16

Abstract

Summary form only given. We give a simple introduction to satisfiability modulo theories intended for non-specialists. No previous background is assumed. The tutorial covers the following topics. 1) Propositional satisfiability. 2) DPLL as the main method for satisfiability checking. 3) Implementations of DPLL. 4) Theories. 5) Decision procedures for theories. Congruence closure, the theory of arrays and linear arithmetic. 6) SMT: satisfiability modulo theories. How to convert a decision procedure for a set of literals to a DPLL modulo theory algorithm. 7) Satisfiability in a combination of theories. Instead of proving theorems, we will try to explain the main ideas using examples. The tutorial serves as a background for the second tutorial by Nikolaj Bjorner "SMT solvers for Testing, Program Analysis and Verification at Microsoft".

Keywords

arrays; computability; digital arithmetic; program diagnostics; program verification; DPLL; SMT; arrays theory; congruence closure; linear arithmetic; program analysis; program verification; propositional satisfiability; satisfiability modulo theories; Arithmetic; Logic; Scientific computing; Surface-mount technology; Testing; decision procedures; propositional logic; satisfiability; satisfiability modulo theory; theory combination;

fLanguage

English

Publisher

ieee

Conference_Titel

Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2009 11th International Symposium on

Conference_Location

Timisoara

Print_ISBN

978-1-4244-5910-0

Electronic_ISBN

978-1-4244-5911-7

Type

conf

DOI

10.1109/SYNASC.2009.65

Filename

5460876