A Technique for Invariant Generation

A. Tiwari, H. Rue{\ss}, H. Sa\"{\i}di, and N. Shankar

To be presented at Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001 , Genova, Italy, April 2001. This paper is © Springer-Verlag. See the Springer LNCS series Homepage.

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.

Errata

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 = {LNCS},
	VOLUME = 2031,
	MONTH = apr,
	YEAR = 2001,
	ADDRESS = {Genova, Italy}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page