Skip to main content
SpringerLink
Log in

Model Checking Guided Abstraction and Analysis

  • Conference paper
Static Analysis (SAS 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1824))

Included in the following conference series:

Abstract

The combination of abstraction and state exploration techniques is the most promising recipe for a successful verification of properties of large or infinite state systems. In this work, we present a general, yet effective, algorithm for computing automatically boolean abstractions of infinite state systems, using decision procedures. The advantage of our approach is that it is not limited to particular concrete domains, but can handle different kinds of infinite state systems. Furthermore, our approach provides, through the use of model checking as a tool for the exploration of the state-space of the abstract system, an automatic way of refining the abstraction until the property of interest is verified or a counterexample is exhibited. We illustrate our approach on some examples and discuss its implementation.

This research was supported by DARPA contract F30602-97-C-0040.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)

    Google Scholar 

  2. Bensalem, S., Lakhnech, Y., Saïdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 323–335. Springer, Heidelberg (1996)

    Google Scholar 

  3. Bjorner, N., Browne, A., Manna, Z.: Automatic Generation of Invariants and Intermediate Assertions. Theoretical Computer Science (1997)

    Google Scholar 

  4. Mani Chandy, K., Misra, J.: Parallel Program Design. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  5. Chou, C.-T.: Simple proof techniques for property preservation via simulation. Information Processing Letters 60(3), 129–134 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  6. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  7. Colon, M., Uribe, T.: Generating finite-state abstractions of reactive systems using decision procedures. In: CAV 1998. LNCS, Springer, Heidelberg (1998)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL (January 1977)

    Google Scholar 

  9. Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven (July 1996)

    Google Scholar 

  10. Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In: Olderog, E.-R. (ed.) IFIP Conference PROCOMET 1994, pp. 561–581 (1994)

    Google Scholar 

  11. Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Dingel, J., Filkorn, T.: Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, Springer, Heidelberg (1995)

    Google Scholar 

  13. Graf, S.: Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distributed Computing (1995)

    Google Scholar 

  14. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)

    Google Scholar 

  15. Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. Technical report, Department of Philosophy (October 1993)

    Google Scholar 

  16. Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)

    Google Scholar 

  17. Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. Technical report, Department of Philosophy, Utrech University, The Netherlands (March 1994)

    Google Scholar 

  18. Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39–50. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Kurshan, R.P.: Computer-aided verification of coordinating processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press (1994)

    Google Scholar 

  20. Lesens, D., Saïdi, H.: Automatic verification of parameterized networks of processes by abstraction. In: Moller, F. (ed.) 2nd International Workshop on Verification of Infinite State Systems: Infinity 1997, Bologna, Italy, July 1997. Electronic Notes in Theoretical Computer Science, vol. 9, Elsevier, Amsterdam (1997)

    Google Scholar 

  21. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6(1) (January 1995)

    Google Scholar 

  22. Manna, Z., Pnueli, A.: The Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

  23. Owre, S., Shankar, N., Rushby, J.M.: A tutorial on specification and verification using pvs. Technical report, Computer Science Laboratory, SRI International (February 1993)

    Google Scholar 

  24. Saïdi, H.: Modular and incremental analysis of concurrent software systems. In: 14th IEEE International Conference on Automated Software Engineering, Cocoa Beach, FL, pp. 92–101. IEEE Computer Society Press, Los Alamitos (1999)

    Chapter  Google Scholar 

  25. Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. System Design Laboratory SRI International, Menlo Park, CA, 94025, USA

    Hassen Saïdi

Authors
  1. Hassen Saïdi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of California, Los Angeles, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Saïdi, H. (2000). Model Checking Guided Abstraction and Analysis. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45099-3_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67668-3

  • Online ISBN: 978-3-540-45099-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation