The Invariant Checker is a tool for the computer aided verification, dedicated, dedicated to the proof of invariance properties of reactive systems. The aim of the tool is to provide a framework combining theorem-proving techniques (Pvs theorem prover) and deductive verification methods. Systems are described as a parallel composition of sequential programs described in a language close to the Dijkstra guarded command language. Program variables can be of any type definable in Pvs. The tool provides automatic generation od invariants, automatic strengthening od invariants and automatic abstarction. The tool is interfaced with ALDÉBARAN, a tool for the analysis of state graphs

• Invariant-Checker.pdf
• Invariant-Checker.ps.gz