InVeSt has been jointly developed by Verimag, University of Kiel and SRI.
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.
Related papers
- Automatic Generation of Invariants. S. Bensalem and Y. Lakhnech . In Formal Methods in System Design 15(1), 1999.
- Construction of Abstract State Graphs with PVS . S. Graf and H. Saidi . In Computer Aided Verification’97, LNCS 1254
- Computing Abstractions of Infinite State Systems Automatically and Compositionally. S. Bensalem, Y. Lakhnech and S. Owre Computer . In Computer Aided Verification’98, LNCS 1427.
- InVeSt : A Tool for the Verification of Invariants. S. Bensalem, Y. Lakhnech and S. Owre . In Computer Aided Verification’98, LNCS 1427.
- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl and Y. Lakhnech. In Computer Aided Verification’99, LNCS 1633.
- Incremental Verification by Abstraction. S. Bensalem, Y. Lakhnech, S. Berezin and S. Owre. To appear in TACAS’01.
Availability
InVeSt is available and distributed for non-profit uses. Contact Yassine Lakhnech or Saddek Bensalem.
