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.
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
(lakhnech@imag.fr) or S. Bensalem (bensalem@imag.fr).