The Stanford Temporal Prover, STeP, supports the computer-aided
formal verification of concurrent and reactive
systems based on temporal specifications.
Reactive systems maintain an ongoing interaction with their environment,
and their specifications are typically expressed as constraints on their
behavior over time.
STeP is not restricted to finite-state systems, but combines
*model checking* with *deductive methods*
to allow for the verification of a broad
class of systems, including parameterized (N-component) circuit
designs, parameterized (N-process) programs, and programs with
infinite data domains.

Finite-state systems can be automatically verified
using modelchecking alone.
For large finite-state or for infinite-state systems,
for which modelchecking is not possible or feasible,
STeP also uses deductive methods:
*Verification rules* [Manna,Pnueli95]
reduce temporal properties to first-order verification conditions.
*Verification diagrams* [Manna,Pnueli94]
are a visual language for guiding, organizing and displaying proofs.
They can be used to construct proofs
hierarchically, starting from a high-level sketch
and proceeding incrementally through layers of greater detail.

STeP also includes techniques for automatic
*invariant generation*
[Bjorner,Browne,Manna97].
Deductive verification
almost always relies on finding, for a given
program and specification, suitably strong
invariants and intermediate assertions.
The system generates bottom-up invariants
automatically by analyzing the program text.
Combining them with the property to be proved,
sufficiently detailed invariants can often be obtained
to carry through the
verification process.

Finally, STeP provides a collection of simplification and decision procedures that automatically check the validity of a large class of first-order and temporal formulas. This degree of automated deduction can handle many of the verification conditions that arise in deductive verification.

The figure above shows an overview of STeP.
The main inputs are a reactive system
(which can be a description of hardware or software)
and a property to be proven about the system,
represented by a temporal logic formula.
Verification can be performed by the modelchecker or by deductive means.
Modelchecking is automatic;
deductive verification is to a large extent automatic for
simple *safety* properties,
while *progress* properties require more user guidance,
usually given in the form of a verification diagram. In all cases, the
automatic prover is responsible for generating and proving the
required verification conditions.
An interactive Gentzen-style theorem prover is used
to establish those verification conditions that
are not proved automatically.

This is the updated manual for release version 1.3.

Technical report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.

Postscript, PDF. © 1995, STeP group.

© Henny Sipma / sipma@cs.stanford.edu Last modified: Thu Mar 29 21:51:34 PST 2001