The Stanford Temporal Prover

An overview of STeP Obtaining STeP The STeP Team Publications
(by year)
(by topic)
Case studies

What is STeP

The Stanford Temporal Prover, STeP, is being developed by the REACT research group to support the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification. Unlike most systems for temporal verification, STeP is not restricted to finite-state systems, but combines model checking with deductive methods to allow the verification of a broad class of systems, including parameterized (N-component) circuit designs, parameterized (N-process) programs, and programs with infinite data domains.

STeP in more detail

The STeP diagram Scope of STeP STeP's interfaces
postscript postscript Large gif

STeP papers:

More publications of the STeP group

This material is based upon work supported by the National Science Foundation under Grant No. 9804100.
Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF)
Stanford's home page Computer Science Department Theory Division