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 [15]. Proving invariance properties is especially crucial for infinite and large finite state systems which escape algorithmic methods. In this paper we present the tool In VeSt which supports the verification of invariance properties of infinite state systems. In VeSt integrates deductive and algorithmic verification principles for the verification of invariance properties as well as abstraction techniques.

• cav98-tool.ps