The Stanford Temporal Prover


An overview of STePObtaining STePThe STeP TeamPublicationsCase 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 diagramScope of STePSTeP's interfaces
postscriptpostscriptLarge gif


STeP papers:

More publications of the STeP group


Acknowledgement
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 pageComputer Science DepartmentTheory Division


step-comments@CS.Stanford.EDU