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

• slides

• 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:

• results of Nelson and Oppen, including Nelson's dissertation
• inclusion of SAT solvers and the DPLL(T) algorithm: Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)
• The SMT-LIB initiative with standardized format, benchmarks, and competitions
• The provers such as Z3 prover

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

Deciding Quantifier-Free FOL

Axioms for Equality

Notes on Congruences

Congruence Closure Algorithm and Correctness

Implementing Congruence Closure

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.