SMT Solvers

Description

SMT (Satisfiabiliy Modulo Theories) is the meeting point of SAT and first-order: by customizing the inevitable trade-off between efficiency and expressiveness, SMT is widely applied in many (industrial) applications. In this tutorial we will introduce the basic principles of state-of-the-art SMT solving and we will show concrete SMT encodings using the standardized language SMTLib 2. In particular, we will discuss the successful DPLL(T) approach and its relation to SAT solving. Then we will give an overview of reasoning with popular theories such as uninterpreted functions with equality, arithmetic, bitvectors, and arrays as well as the combination of different theories. Various application problems will be encoded and solved using these theories illustrating how SMT can be practically used.

Period	15 Apr 2016
Event title	RiSE & LogiCS Spring School on Logic and Verification 2016
Event type	Conference
Location	AustriaShow on map