Construction of abstract state graphs with PVS

  • Susanne Graf
  • Hassen Saidi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.

Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ1, ..., g4 l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕi or ¬ϕi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.


abstract interpretation state graph exploration theorem proving 


  1. [BBC+96]
    N. Bjorner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H. Sipma, and T. Uribe. Step: Deductive-algorithmic verification of reactive and realtime systems. In CAV'96. LNCS 1102, 1996.Google Scholar
  2. [BBL97]
    K. Baukus, S. Bensalem, and Y. Lakhnech. A PVS based tool for the verification of invariants. submitted to CAV'97.Google Scholar
  3. [BLS96]
    S. Bensalem, Y. Lakhnech, and H. Saidi, Powerful techniques for the automatic generation of invariants. In CAV'96, LNCS 1102, 1996.Google Scholar
  4. [CC77]
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, January 1977.Google Scholar
  5. [CGL94]
    E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994.Google Scholar
  6. [CM88]
    K. M. Chandy and J. Misra. Parallel Program Design. 1988.Google Scholar
  7. [Dam96]
    D. Dams. Abstract interpretation and partition refinement for model checking. Phd Thesis, Technical University of Eindhoven, July 1996.Google Scholar
  8. [DF95]
    J. Dingel and Th. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In CAV'95. LNCS 939, 1995.Google Scholar
  9. [DGG93]
    D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In CAV'93, LNCS 697, 1993.Google Scholar
  10. [DOTY96]
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, LNCS 1066, 1996.Google Scholar
  11. [FGK+96]
    J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier and M. Sighireanu. CADP (Caesar/Aldébaran Development Package): A protocol validation and verification toolbox. In CAV'96. LNCS 1102.Google Scholar
  12. [GL93]
    S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV'93. LNCS 697, 1993.Google Scholar
  13. [Gra95]
    S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. accepted to Distributed Computing.Google Scholar
  14. [GS96]
    S. Graf and H. Saidi. Verifying invariants using theorem proving. In CAV'96, LNCS 1102, 1996.Google Scholar
  15. [GvdP93]
    J.F Groote and J. van de Pol. A bounded retransmission protocol for large data packets. Technical Report Logic Group 100, Utrecht University, 1993.Google Scholar
  16. [HGD95]
    H. Hungar, O. Grumberg, and W. Damm. What if model checking must be truly symbolic. In TACAS'95. LNCS 1019, 1995.Google Scholar
  17. [HH95]
    T. Henzinger and P.H. Ho. Hytech: the Cornell hybrid technology tool. In Hybrid Systems II. LNCS 999, 1995.Google Scholar
  18. [HPR94]
    N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In SAS'94. LNCS 864.Google Scholar
  19. [HS96]
    K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods in Europe'96, 1996.Google Scholar
  20. [HSV94]
    L. Helmink, M. Sellink, and F. Vaandrager. Proof-checking a data link protocol. Technical report CS-R9420, CWI, 1994.Google Scholar
  21. [KDG95]
    P. Kelb, D. Dams, and R. Gerth. Efficient symbolic model-checking for the full μ-calculus using compositional abstractions. Tech Rep 31, TU Eindhoven, 1995.Google Scholar
  22. [Kur94]
    R.P. Kurshan. Computer-Aided Verification of Coordinating processes, the automata theoretic approach. Princeton Series in Computer Science. 1994.Google Scholar
  23. [LGS+95]
    C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, Vol 6, Iss 1, 1995 Google Scholar
  24. [Sa97]
    H. Saïdi. The invariant checker: Automated deductive verification of reactive systems. In this volume.Google Scholar
  25. [Sif82]
    Joseph Sifakis. A unified approach for studying the properties of transition systems. TCS 18, 1982.Google Scholar
  26. [SOR93]
    N. Shankar, S. Owre, and J.M. Rushby. A Tutorial on Specification and Verification using PVS. SRI International, Menlo Park, CA, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Susanne Graf
    • 1
  • Hassen Saidi
    • 1
  1. 1.Centre EquationVERIMAGGrenoble-Gières

Personalised recommendations