Colloquium - An Introduction to SMT Solvers and Their Applications (Part 1/2)

118 MLH
Andrew Reynolds
University of Iowa | Computer Science

Satisfiability Modulo Theories (SMT) solvers are used as backend reasoning engines by a growing number of modern formal methods applications, including software verification tools, interactive theorem provers and symbolic execution engines. SMT solvers are useful in such applications due to their ability to efficiently reason in theories such as arithmetic, arrays, inductive datatypes and unbounded character strings. This talk will cover the basics of how SMT solvers work. It will cover the basics of the DPLL(T) algorithm for quantifier-free satisfiability in the presence of combinations of background theories. It will also demonstrate examples of how SMT solvers can be used for applications in verification, symbolic execution and software synthesis.


Andrew Reynolds is a research scientist at the University of Iowa and an active developer of the state-of-the-art Satisfiability Modulo Theories (SMT) solver CVC4. He received his doctorate at the University of Iowa under the supervision of Cesare Tinelli, and did a postdoc at Ecole Polytechnique Fédérale de Lausanne (EPFL) in Switzerland. His research interests are in various aspects of SMT, including decision procedures, proofs, and approaches for quantified formulas.