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:

• generation of proof obligations (system or property dependent)
• automatic generation of invariants (used in proofs)
• automatic predicate abstraction

Presentation

Bibliography (abstracts and electronic versions here )

• [BGL03] Abstraction as the Key for Invariant Verification. Saddek Bensalem, Susanne Graf, Yassine Lakhnech In Int. Symposium on Verification celebrating Zohar Manna's 64th Birthday , LNCS 2772, Springer Verlag 2003
• [Sai98] Combinaison de Methodes Deductives et Algorithmiques pour la Verication. H.Saidi. In PhD thesis, obtained from Universite Joseph Fourier - Grenoble I, January 27, 1998 in Grenoble
• [Sai97b] Automated Deductive Verification of parallel Systems. H.Saidi. In Proceedings of the Fourth NASA Langley Formal Methods Workshop (Lfm'97), Hampton, Virginia, September 1997.
• [GS97] Construction of abstract state graphs with PVS. S.Graf, H.Saidi. In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.
• [Sai97] The Invariant-Checker : Automated Deductive Verification of Reactive Systems (Tool Presentation). H.Saidi. In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.
• [LS97] Automatic Verification of Parameterized Networks of Processes by Abstraction D. Lesens, H.Saidi. In Proceedings of the 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97), Bologna, Italy, July 1997.
• [GS96] Verifying Invariants Using Theorem Proving. S.Graf, H.Saidi. In Proceedings of 8th Conference on Computer-Aided Verification (CAV'96), Rutgers University, New Jersey, July 1996.
• [BLS96] Powerful Techniques for the Automatic Generation of Invariants. S.Bensalem, Y.Lakhnech, H.Saidi. In Proceedings of 8th Conference on Computer-Aided Verification (CAV'96), Rutgers University, New Jersey, July 1996.
• [Sai96] A Tool for Proving Invariance Properties of Concurrent Systems Automatically (Tool Presentation). H.Saidi In Proceedings of 2nd International Workshop, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Passau, Germany, March 1996. Lecture Notes in Computer Science 1055, pages 412--416, Springer-Verlag.
• [LGBBS95] Property Preserving Abstractions for the Verification of Concurrent Systems. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem In Formal Methods in System Design , Vol 6, Iss 1, January 1995
• [GL93] Program Verification using compositional Abstraction. S. Graf, C. Loiseaux In TAPSOFT 93, joint conference CAAP/FASE ,LNCS 668, Springer Verlag

Related Work

• [MP95] Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

• A few small Examples.
  
• Verification of a Bounded Retransmission Protocol (BRP).
  

• the INVEST tool which has been developed in parallel with the invariant checker (see also [BGL03]) implements also predicate abstractions
• the tools of the SLAM project include a tool for building predicate abstractions as in the invariant checker. SLAM applies this to software written in C, in particular to device drivers.