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.