The information listed on this page refers to the state of the tool in '99. For more recent information, please use the following link:

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

---

InVeSt - VERIMAG, Univ. of Kiel, SRI

Name: InVeSt (Invariants Verification System)

Main Functionalities

Verification of invariance properties of infinite state systems

Derived Functionalities

Automatic generation of invariants

Compositional computation of abstractions

Reachability analysis of lossy communicating systems

Description

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.

Related papers

"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.
 

Availability

InVeSt will be shortly available and distributed to academic institutions for non-profit uses.
Contact person: S. Bensalem (Saddek.Bensalem@imag.fr).