The Stanford Temporal Prover
An overview of STeP | Obtaining STeP | The STeP Team | Publications | Case studies |
---|
| | | | |
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.
- Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomas Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. To appear in Formal Methods in System Design.
- Nikolaj Bjorner, Zohar Manna, Henny Sipma, Tomas Uribe. Deductive Verification of Real-Time Systems Using STeP. Technical Report STAN-CS-TR-98-1616, Computer Science Department, Stanford University, December 1998. 40 pages.
- Zohar Manna and the STeP group. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In 8th International Conference on Computer-Aided Verification, vol. 1102 of LNCS, pp. 415-418, Springer-Verlag, July 1996. 4-page description.
- Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover (Educational Release), User's Manual. Technical report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995. 138 pages.
- Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover (2-page abstract). In TAPSOFT'95: Theory and Practice of Software Development, vol. 915 of Lecture Notes in Computer Science, pp. 793-794, May 1995.
- Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994. 44 pages.
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 page | Computer Science Department | Theory Division |
---|
| | |
step-comments@CS.Stanford.EDU