Skip to main content
SpringerLink
Log in

Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover

  • Conference paper
Book cover Theorem Proving in Higher Order Logics (TPHOLs 2003)

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

Included in the following conference series:

Abstract

Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model checking algorithms may be embedded in a theorem prover to take advantage of the comparatively secure environment without incurring an unacceptable performance penalty.

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. Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Combining theorem proving and trajectory evaluation in an industrial environment. In: Design Automation Conference (DAC), pp. 538–541. ACM/IEEE (1998)

    Google Scholar 

  2. Agerholm, S., Skjodt, H.: Automating a model checker for recursive modal assertions in HOL. Technical Report 92, Aarhus University (January 1990)

    Google Scholar 

  3. Bryant, R.E.: Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)

    Article  Google Scholar 

  4. The BuDDy ROBDD Package (2002), http://www.itu.dk/research/buddy

  5. Burch, J.R., Clarke, E.M., Long, D.E.: Representing circuits more efficiently in symbolic model checking. In: Proceedings of the ACM Design Automation Conference (1991)

    Google Scholar 

  6. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5(2), 56–68 (1940)

    Article  MATH  MathSciNet  Google Scholar 

  7. Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstractionrefinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 265. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  9. 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 

  10. Cleaveland, R.: Tableau-based model checking in the propostional mu-calculus. Extended Abstract, Computer Science Department, University of Sussex (1988)

    Google Scholar 

  11. Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design (November 2002)

    Google Scholar 

  12. Dingel, J., Filkorn, T.: Model checking for infinite state systems using data abtraction, assumption-commitment style reasoning and theorem proving. In: Proceedings of the 1995 Workshop on Computer Aided Verification. LNCS, vol. 939, pp. 54–69. Springer, Heidelberg (1995)

    Google Scholar 

  13. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: 1st Annual Symposium on Logic in Computer Science, pp. 267–278. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  14. Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proceedings of the 14th Logic in Computer Science Conference, pp. 193–202. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  15. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing, Special issue in honour of Rod Burstall (2001)

    Google Scholar 

  16. Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)

    Google Scholar 

  17. Gordon, M.J.C.: Programming combinations of deduction and bdd-based symbolic calculation. LMS Journal of Computation and Mathematics (August 2002)

    Google Scholar 

  18. Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  19. Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)

    Google Scholar 

  20. The HOL Proof Tool (2003), http://hol.sf.net

  21. Holzmann, G.J., Peled, D.: The state of spin. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 385–389. Springer, Heidelberg (1996)

    Google Scholar 

  22. SRI International. Prototype verification system, http://pvs.csl.sri.com

  23. Joyce, J., Seger, C.: The HOL-Voss system: Model checking inside a generalpurpose theorem prover. In: Higher Order Logic Theorem Proving and its Applications. LNCS, vol. 780, pp. 185–198. Springer, Heidelberg (1993)

    Google Scholar 

  24. Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  25. Kurshan, R.P., Lamport, L.: Verification of a multiplier: 64 bits and beyond. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 166–180. Springer, Heidelberg (1993)

    Google Scholar 

  26. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  27. Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: Pvs: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  28. Pnueli, A., Rua, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (2001)

    Google Scholar 

  29. Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking and automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939. Springer, Heidelberg (1995)

    Google Scholar 

  30. Saidi, H.: Model checking guided abstraction and analysis. In: Proceedings of the 7th International Static Analysis Symposium (2000)

    Google Scholar 

  31. Seger, C.-J.H.: Voss - a formal hardware verification system: User’s guide. Technical report, The University of British Columbia, UBC-TR-93-45 (December 1993)

    Google Scholar 

  32. Skolem, T.: Some remarks on axiomatised set theory. In: van Heijenoort, J. (ed.) From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, pp. 290–301. Harvard University Press (1967)

    Google Scholar 

  33. Sprenger, C.: Deductive Local Model Checking. PhD thesis, Computer Networking Laboratory,Swiss Federal Institute of Technology, Lausanne, Switzerland (2000)

    Google Scholar 

  34. Stanford Temporal Prover, http://www-step.stanford.edu

  35. Stirling, C., Walker, D.J.: Local model checking in the modal mu-calculus. In: Díaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351. Springer, Heidelberg (1989)

    Google Scholar 

  36. Symbolic Model Prover, http://www.cs.cmu.edu/~modelcheck/symp.html

  37. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955)

    MATH  MathSciNet  Google Scholar 

  38. Uribe, T.E.: Combinations of model checking and theorem proving. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol. 1794, pp. 151–170. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  39. Winskel, G.: A note on model checking in the modal ν-calculus. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Cambridge Computer Laboratory, William Gates Building, 15 JJ Thomson Avenue, Cambridge, CB3 0FD, UK

    Hasan Amjad

Authors
  1. Hasan Amjad
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Information Security Group, Dep. of Computer Science, ETH Zurich, Switzerland

    David Basin

  2. Computer Science Dept., Saarland University, 66123, Saarbrücken, Germany

    Burkhart Wolff

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Amjad, H. (2003). Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_11

Download citation

  • DOI: https://doi.org/10.1007/10930755_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40664-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation