An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems

Zohar Manna, Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Mark Pichora, Henny Sipma, Tomas Uribe

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.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Thu Mar 29 18:25:20 PST 2001