Verification Conditions
This page presents a small set of verification conditions generated
by STeP (The Stanford Temporal Prover)
during the deductive verification of temporal properties of reactive systems,
as part of research done in
Zohar Manna's REACT group.
The problems are presented here without an axiomatization of the
theories involved. These are: equality, real and integer arithmetic, arrays,
and datatypes (finite-domain, for these examples).
How to deal with these (standard) theories is left as a parameter of
proposed solutions to these problems (probably the most important one).
- Easy: Two verification conditions
to prove mutual exclusion
for the 2-process Bakery algorithm.
- Medium: Two
verification conditions for simple properties of
a water-level controller (a hybrid system), courtesy of
Henny Sipma.
- Hard:
Eight verification conditions
for the verification of a leader election
algorithm, courtesy of
Nikolaj Bjørner.
(The hard part is duplicating and instantiating quantifiers correctly;
at the ground level, they are relatively easy, using decision
procedures.)
The STeP Validity Checker
I suspect that we have dealt with the test problems in this page
in a different manner from others classes of problems in this workshop:
with the development of specialized decision procedures and
validity checkers
that attempt to prove as many verification conditions
automatically as possible.
Thus, the iterative solution process has been not so much in the use of the tool
(though we do have an interactive prover),
but the development of the tool itself.
A position statement
about the challenges that such verification problems present
was included
in the 1997 CADE Workshop on
Automated Theorem Proving in Software Engineering
(N.S. Bjørner and T.E. Uribe, Quantifiers, Decision Procedures, and the
Verification of Reactive Systems, 1997).
You can try out an
on-line demo of this validity checker, wich includes a number of
other verification conditions of interest, including some for verifying
the
famous SRT division table (a.k.a. the Pentium Bug).
Tomás E. Uribe
uribe@CS.Stanford.EDU
Last modified: April 15, 1998.