SMT Solvers

Part I

First, from 10:15 to 10:50, we present the basic technology behind the SMT solvers.

  • QF formula is satisfiable iff some disjunct is SAT
  • use SAT solver to cleverly enumerate disjuncts
  • suffices to solve conjunctions
  • separate mixed terms in atomic formulas using fresh variables (flatten)
  • each theory solves its own conjuncts

Milestones in SMT solver development:

Introduction from Selected VeriFun slides (Full VeriFun slides are here)

Deciding Quantifier-Free FOL

Part II

Dr. Filip Maric will present the following work, which explains one of the core techniques used in handling linear numerical constraints within SMT solvers, as well as their verification in the Isabelle theorem prover. The presentation starts at 11:00 and will last for about one hour.

We present a Simplex-based solver for quantifier-free linear arithmetic over rationals (QF-LRA), described originally by Dutertre and de Moura. This solver is incremental, efficiently integrated in the DPLL(T) framework and used by many state-of-the art SMT solvers. Next, we present some elements of the interactive theorem prover Isabelle/HOL. Finally, we demonstrate some steps in verification of the Simplex solver within Isabelle/HOL, using the technique of stepwise program and data refinement.