Report Number: CS-TR-95-1562
Institution: Stanford University, Department of Computer Science
Title: STeP: The Stanford Temporal Prover (Educational Release) User's Manual
Author: Bjorner, Nikolaj
Author: Browne, Anca
Author: Chang, Eddie
Author: Colon, Michael
Author: Kapur, Arjun
Author: Manna, Z ohar
Author: Sipma, Henny B.
Author: Uribe, Tomas E.
Date: November 1995
Abstract: The STeP (Stanford Temporal Prover) system supports the computer-aided verification of reactive and real-time systems. It combines deductive methods with algorithmic techniques to allow the verification of a broad class of systems, including infinite-state systems and parameterized N-process programs. STeP provides the visual language of verification diagrams that allow the user to construct proofs hierarchically, starting from a high-level proof sketch. The availability of automatically generated bottom-up and top-down invariants and an integrated suite of decision procedures allow most verification conditions to be checked without user intervention.
http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1562/CS-TR-95-1562.pdf