Saddek Bensalem, Yassine Lakhnech, and, Hassen Saïdi

Powerful Techniques for the Automatic Generation of Invariants

In Proceedings of 8th Computer-Aided Verification, July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.


When proving invariance properties of programs one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable on sequential transition systems and allows to derive so-called local invariants, i.e. predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows to combine local invariants of the sequential components to obtain local invariants of the global systems. Furthermore, a refined strengthening technique is presented that allows to avoid the problem of size-increase of the considered predicates which is the main drawback of the usual strengthening technique. The proposed techniques are illustrated by examples.

Click here to get the postscript file of the full paper.