CADE-18 tutorial
July 25th, 2002

On Shostak's Approach for Combining Decision Procedures

Decision procedures are at the core of many verification systems including ACL2, PVS, STeP, SVC, or Z/Eves. These procedures are used to automatically discharge verification conditions such as

f(f(x)-f(y)) /= f(z) & y <= x & y >= x+z & z >= 0 => false,

that involve reasoning in the combination of theories including equality over uninterpreted terms, arithmetic and the Boolean theory. This tutorial reviews the fundamental decision procedures for equality reasoning and presents the basic techniques for combining decision procedures.

In particular, we will cover:

  • Online and offline congruence closure
  • Solvers and canonizers
  • Nelson-Oppen and Shostak combination algorithms
  • Combining Groebner basis computation with congruence-closure
  • Quantifier-elimination
  • The use of decision procedures in proof search
  • The Icansolve (ICS) decision procedures
This tutorial is based on five years of theoretical research and over a decade of practical experience building and using decision procedures.