Lecture Notes in Computer Science, Volume 2031.
From TACAS 2001 - Tools and Algorithms for the Construction and Analysis of Systems.
Edited by Tiziana Margaria and Wang Yi.
Springer-Verlag, Genova, Italy.
April, 2001.
Pages 113–127.

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.

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

• tacas01.ps.gz