 | |
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.
Organizers | |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
