Sample problems for CADE-98 Workshop:
Problem-Solving with Automated Deduction

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).

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


Last modified: April 15, 1998.