SRI International Computer Science Laboratory

InVeSt: A Tool for the Verification of Invariants

Saddek Bensalem, Yassine Lakhnech, and Sam Owre

Presented at Computer-Aided Verification (CAV'98), Vancouver, BC, Canada, June/July 1998. Springer-Verlag Lecture Notes in Computer Science Vol. 1427, pp 505-510.


A very important class of properties of reactive systems consists of invariance properties which state that all reachable states of the considered system satisfy some given property. Indeed, every safety property can be reduced to an invariance property and to prove progress properties one needs to establish invariance properties. Proving invariance properties is especially crucial for infinite and large finite state systems which escape algorithmic methods. In this paper we present the tool InVeSt which supports the verification of invariance properties of infinite state systems. InVeSt integrates deductive and algorithmic verification principles for the verification of invariance properties as well as abstraction techniques.

postscript(90kb) or gzipped postscript(28kb)

BibTeX Entry

	AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
	TITLE = {{InVeSt: A} Tool for the Verification of Invariants},
	PAGES ={505--510},

Sam Owre: