The Stanford Temporal Prover, STeP, is a tool for the com\-puter-aided formal verification of reactive systems, including real-time and hybrid systems, based on their temporal specification. STeP integrates methods for deductive and algorithmic verification, including model checking, theorem proving, automatic invariant generation, abstraction and modular reasoning. We describe the most recent version of STeP, Version~2.0.
In Tool Support for System Specification, Development and Verification, Advances in Computing Science, pp 174-188, Springer Verlag, 1999.
Postscript, PDF. © 1998, Springer Verlag.