Hassen Saïdi
The Invariant-Checker : Automated Deductive Verification of Reactive Systems.
In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.
Abstract
Tool Presentation. The Invariant Checker is a tool for the computer aided verification, 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's guarded command language. Program variables can be of any type definable in PVS. The tool provides automatic generation of invariants, automatic strengthening of invariants and automatic abstraction. The tool is interfaced with Ald\'ebaran, a tool for the analysis of state graphs.