Abstract. STeP, the Stanford Temporal Prover, supports the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB99]. Automated model checking is combined with computer-aided deductive methods to allow for the verification of a broad class of systems, including parameterised ( N -component) circuit designs, parameterised ( N -process) programs, and programs with infinite data domains.

Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and on strengthening given properties of the system. This can be achieved by two dual approaches: The bottom-up method performs an abstract forward propagation (computation) of the system, generating auxiliary assertions; the top-down method performs an abstract backward propagation to strengthen given properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. Approximation techniques are often needed to complete the verification. We give an overview of known methods for generation of auxiliary invariants in the verification of invariance properties. We extend these methods, by formalizing and analyzing a general verification rule that uses assertion graphs to generate auxiliary assertions for the verification of general safety properties.