AUTOMATIC-GENERATION OF INVARIANTS AND INTERMEDIATE ASSERTIONS

Verifying temporal specifications of reactive and concurrent systems c ommonly relies on generating auxiliary assertions and on strengthening given properties of the system. This can be achieved by two dual appr oaches: 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 gi ven properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. Approximation techniq ues are often needed to complete the verification. We give an overview of known methods for generation of auxiliary invariants in the verifi cation of invariance properties. We extend these methods, by formalizi ng and analyzing a general verification rule that uses assertion graph s to generate auxiliary assertions for the verification of general saf ety properties.