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.
Abstract
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
@inproceedings{Bensalem98:InVeSt,
AUTHOR = {Saddek Bensalem and Yassine Lakhnech and Sam Owre},
TITLE = {{InVeSt: A} Tool for the Verification of Invariants},
PAGES ={505--510},
CROSSREF = {CAV98}
}
Sam Owre:
Owre@csl.sri.com