Automatic Generation of Invariants and Intermediate Assertions

Nikolaj Bjorner, Anca Browne, Zohar Manna

Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and on strengthening given properties of the system. Two dual approaches find solutions to these problems: 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. An approximate analysis can often supply enough information to complete the verification.

The paper overviews some of the exact and approximate analysis methods to generate and strengthen assertions for the verification of invariance properties. By formulating and analyzing a generic safety verification rule, we extend these methods to the verification of general temporal safety properties.

Appeared inTheoretical Computer Science, vol. 173(1), pp. 49-87, February 1997.
Original version appeared in 1st International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 976, Cassis, France, pp. 589-623, September 1995.

Postscript, PDF. © 1997, Elsevier Science B.V.


Last modified: Thu Mar 29 16:29:45 PST 2001