Skip to main content
SpringerLink
Log in

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

  • Conference paper
  • First Online:
Automated Deduction—CADE-18 (CADE 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2392))

Included in the following conference series:

Abstract

We investigate the combination of propositional SAT checkers with domain-specific theorem provers as a foundation for bounded model checking over infinite domains. Given a program M over an infinite state type, a linear temporal logic formula ϕ with domain-specific constraints over program states, and an upper bound k, our procedure determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification ϕ. This problem can be reduced to the satisfiability of Boolean constraint formulas. Our verification engine for these kinds of formulas is lazy in that propositional abstractions of Boolean constraint formulas are incrementally refined by generating lemmas on demand from an automated analysis of spurious counterexamples using theorem proving. We exemplify bounded model checking for timed automata and for RTL level descriptions, and investigate the lazy integration of SAT solving and theorem proving.

This research was supported by SRI International internal research and development, the DARPA NEST program through Contract F33615-01-C-1908 with AFRL, and the National Science Foundation under grants CCR-00-86096 and CCR-0082560.

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. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. 5th Symp. on Logic in Computer Science (LICS 90), pages 414–425, 1990.

    Google Scholar 

  2. C. W. Barrett, D. L. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, 2002. To be presented at CAV 2002.

    Google Scholar 

  3. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zh. Symbolic model checking without BDDs. LNCS, 1579, 1999.

    Google Scholar 

  4. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.

    Google Scholar 

  5. R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. LNCS, 1633:470–482, 1999.

    Google Scholar 

  6. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. LNCS, 1855:154–169, 2000.

    Google Scholar 

  7. E.M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, 2001.

    Article  MATH  Google Scholar 

  8. F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking in an industrial setting. LNCS, 2101:436–453, 2001.

    Google Scholar 

  9. Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Symposium on Logic in Computer Science, pages 51–60. IEEE, 2001.

    Google Scholar 

  10. J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: Integrated Canonizer and Solver. LNCS, 2102:246–249, 2001.

    Google Scholar 

  11. Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.

    Google Scholar 

  12. A. Goel, K. Sajid, H. Zhou, and A. Aziz. BDD based procedures for a theory of equality with uninterpreted functions. LNCS, 1427:244–255, 1998.

    Google Scholar 

  13. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, June 1994.

    Google Scholar 

  14. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction. ACM SIGPLAN Notices, 31(1):58–70, 2002.

    Article  Google Scholar 

  15. Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291–314, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  16. Yassine Lachnech, Saddek Bensalem, Sergey Berezin, and Sam Owre. Incremental verification by abstraction. LNCS, 2031:98–112, 2001.

    Google Scholar 

  17. M.O. Möller, H. Rueß, and M. Sorea. Predicate abstraction for dense real-time systems. Electronic Notes in Theoretical Computer Science, 65(6), 2002.

    Google Scholar 

  18. O. Möller and H. Rueß. Solving bit-vector equations. LNCS, 1522:36–48, 1998.

    Google Scholar 

  19. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC’01), June 2001.

    Google Scholar 

  20. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.

    Article  MATH  Google Scholar 

  21. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.

    Google Scholar 

  22. David A. Plaisted and Steven Greenbaum. A structure preserving clause form translation. Journal of Symbolic Computation, 2(3):293–304, September 1986.

    Google Scholar 

  23. A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. LNCS, 1633:455–469, 1999.

    Google Scholar 

  24. H. Rueß and N. Shankar. Deconstructing Shostak. In 16th Symposium on Logic in Computer Science (LICS 2001). IEEE Press, June 2001.

    Google Scholar 

  25. Vlad Rusu and Eli Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. LNCS, 1579:178–192, 1999.

    Google Scholar 

  26. H. Saïdi. Modular and incremental analysis of concurrent software systems. In 14th IEEE International Conference on Automated Software Engineering, pages 92–101. IEEE Computer Society Press, 1999.

    Google Scholar 

  27. Robert Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769–779, October 1981.

    Google Scholar 

  28. A. P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6(5):495–512, 1994.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025, USA

    Leonardo de Moura, Harald Rueß & Maria Sorea

  2. University of Ulm, Germany

    Maria Sorea

Authors
  1. Leonardo de Moura
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Harald Rueß
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maria Sorea
    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 Manchester, Oxford Rd, Manchester, M13 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Moura, L., Rueß, H., Sorea, M. (2002). Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-45620-1_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45620-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation