STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems

Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colon, Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe

The Stanford Temporal Prover, STeP, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems. STeP uses verification rules, verification diagrams, automatically generated invariants, model checking, and a collection of decision procedures to verify finite- and infinite-state systems.

In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 415-418, Springer-Verlag, July 1996.

Postscript, PDF. © 1996, Springer Verlag.


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