http://www-verimag.imag.fr/~async/INVEST

InVeSt - VERIMAG, Univ. of Kiel, SRI

Verification of invariance properties of infinite state systems

Automatic generation of invariants

Compositional computation of abstractions

Reachability analysis of lossy communicating systems

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. Proving invariance properties is especially crucial for infinite and large finite state systems which escape algorithmic methods. The tool box InVeSt supports the verification of invariance properties of infinite state systems. It integrates deductive and algorithmic verification principles for the verification of invariance properties as well as abstraction techniques. InVeSt uses the theorem prover PVS as an oracle for discharging automatically generated verification conditions. InVeSt contains several closely interconnected components:

**SIG**(Structural Invariants Generator) generates structural invariants from a given description of a system;**DP**(Deductive Prover) implements a general proof rule which integrates deductive reasoning, model-checking and abstraction techniques;**CASC**(Compositional Abstract System Constructor) computes compositionally a safe abstract system from a given concrete system and an abstraction function;**CEA**(Counter Example Analyzer) analyses counter examples generated when model-checking an abstract system to decide whether the concrete system does not satisfy the invariant to be checked, the abstract function is too coarse or the abstract system is too non-deterministic;**LCS**(Lossy Communicating Systems) computes the set of the reachable states of finite automata communicating via lossy channels.

"Automatic Generation of Invariants"

S. Bensalem and Y. Lakhnech

Formal Methods in System Design 15(1), 1999.

"Construction of Abstract State Graphs with PVS"

S. Graf and H. Saidi

Computer Aided Verification'97, LNCS .1254

"Computing Abstractions of Infinite State Systems Automatically
and Compositionally"

S. Bensalem, Y. Lakhnech and S. Owre

Computer Aided Verification'98, LNCS. 1427.

"InVeSt : A Tool for the Verification of Invariants"

S. Bensalem, Y. Lakhnech and S. Owre

Computer Aided Verification'98, LNCS. 1427.

"On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels"

P. Abdulla, A. Bouajjani and B. Jonsson

Computer Aided Verification'98, LNCS. 1427.

"Symbolic Verification of Lossy Channel Systems: Application to
the Bounded Retransmission Protocol"

P. Abdulla, A. Annichini and A. Bouajjani

TACAS'99, LNCS 1579.

**InVeSt** will be shortly available and distributed to academic
institutions for non-profit uses.

Contact person: S. Bensalem (Saddek.Bensalem@imag.fr).