Advertisement

The invariant checker: Automated deductive verification of reactive systems

  • Hassen Saïdi
Tool Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Keywords

Proof Strategy Typing Context Proof Rule Temporal Logic Formula Mutual Exclusion Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [BLS96]
    S. Bensalem, Y. Lakhnech, and H. Saïdi. Powerful Techniques for the Automatic Generation of Invariants. In Conference on Computer Aided Verification CAV'96, LNCS 1102, July 1996.Google Scholar
  2. [FGK+96]
    J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier and M. Sighireanu. CADP (Cæsar/Aldébaran Development Package): A protocol validation and verification toolbox. In CAV 1996. LNCS 1102, 1996.Google Scholar
  3. [GS96]
    S. Graf and H. Saïdi. Verifying invariants using theorem proving. In Conference on Computer Aided Verification CAV'96, LNCS 1102, July 1996.Google Scholar
  4. [GS97]
    S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In this volume.Google Scholar
  5. [MP95]
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.Google Scholar
  6. [OSR93a]
    S. Owre, N. Shankar, and J. M. Rushby. A Tutorial on Specification and Verification Using PVS. Computer Science Laboratory, SRI International, February 1993.Google Scholar
  7. [Saï96]
    H. Saïdi. A Tool for Proving Invariance Properties of Concurrent Systems Automatically. In TACAS'96, LNCS 1056, Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Hassen Saïdi
    • 1
  1. 1.Centre EquationVERIMAGGrenoble-Gières

Personalised recommendations