A Technique for Invariant Generation

Presented at TACAS'01, Genova, Italy, April 2001. © Springer-Verlag.

---

Authors

Ashish Tiwari, Harald Rueß, Hassen Saidi, and N. Shankar

Abstract

Most of the properties established during verification are either invariants or depend crucially on invariants. The effectiveness of automated formal verification is therefore sensitive to the ease with which invariants, even trivial ones, can be automatically deduced. While the strongest invariant can be defined as the least fixed point of the strongest post-condition of a transition system starting with the set of initial states, this symbolic computation rarely converges. We present a method for invariant generation that relies on the simultaneous construction of least and greatest fixed points, restricted widening and narrowing, and quantifier elimination. The effectiveness of the method is demonstrated on a number of examples.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{TRSS:TACAS01,
        TITLE = {A Technique for Invariant Generation},
        AUTHOR = {A. Tiwari and H. Rue{\ss} and H. Sa\"{\i}di and N. Shankar},
        BOOKTITLE = {TACAS 2001 - Tools and Algorithms for the Construction and Analysis of Systems},
        EDITOR = {Tiziana Margaria and Wang Yi},
        PAGES = {113--127},
        PUBLISHER = {Springer-Verlag},
        SERIES = {Lecture Notes in Computer Science},
        VOLUME = 2031,
        MONTH = apr,
        YEAR = 2001,
        ADDRESS = {Genova, Italy}
}

Errata

---

Harald Ruess: ruess@csl.sri.com