The Invariant Checker

The Invariant-Checker - Automated Deductive Verification and Abstraction of Reactive Systems

The Invariant-Checker is a tool dedicated to both predicate abstraction and verification of invariance properties of reactive systems using a combination of theorem-proving and model checking techniques. The tool is built as a front end for the PVS theorem prover. The tool includes the following features:


A more detailed presentation can be found HERE.

Bibliography (abstracts and electronic versions here )

Related Work

Case studies


An experimental version may be available on request. Notice that not much developments have been done since 2000. Some of the functionalities of the Invariant-Checker, but for different input formats or based on slightly different techniques are available, for example, in
Notice that contrary to Invariant checker, the above mentioned tools are intended for the case where each variable is abstracted individually (or abstractions ar at least local to some component), whereas we intended the tool to be used for building global control abstractions and the used of abstractions based on global predicates. For details and availability, please contact: or

Back to Susanne Graf's home page
Susanne Graf (
Last modified: Thu Dec 21 18:50:56 MET 2006