Skip to main content
SpringerLink
Log in

Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers

  • Conference paper
Model Checking Software (SPIN 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3925))

Included in the following conference series:

Abstract

C Bounded Model Checking (CBMC) has proven to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property and (ii) use state-of-the-art SAT solvers to check the resulting formulae for satisfiability. In this paper we propose a generalisation of the CBMC approach based on an encoding into richer (but still decidable) theories than propositional logic. We show that our approach may lead to considerably more compact formulae than those obtained with CBMC. We have built a prototype implementation of our technique that uses a Satisfiability Modulo Theories (SMT) solver to solve the resulting formulae. Computer experiments indicate that our approach compares favourably with and on some significant problems outperforms CBMC.

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. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC 2003, pp. 368–371. ACM Press, New York (2003)

    Google Scholar 

  3. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Nelson, G., Oppen, D.: Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1, 245–257 (1979)

    Article  MATH  Google Scholar 

  5. Shostak, R.E.: Deciding Combinations of Theories. Journal of ACM 31, 1–12 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  6. Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proceedings of LICS 2001. IEEE, Los Alamitos (2001)

    Google Scholar 

  8. Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Information and Computation 183, 140–164 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 65–80. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Cyrluk, D., Möller, O., Rueß, H.: An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  11. Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proceedings of DAC 1998, pp. 522–527 (1998)

    Google Scholar 

  12. Grumberg, O. (ed.): CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  13. Möller, O., Rueß, H.: Solving Bit-Vector Equations. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 36–48. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Bozzano, M., Bruttomesso, R., Cimatti, A., Franzen, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL Constructs for MATHSAT: a Preliminary Report. In: Armando, A., Cimatti, A. (eds.) 3rd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005). Electronic Notes in Theoretical Computer Science, vol. 144 (2005)

    Google Scholar 

  15. Clarke, E., Kroening, D., Yorav, K.: Behavioral Consistency of C and Verilog Programs. Technical Report CMU-CS-03-126, Computer Science Department, School of Computer Science, Carnegie Mellon University (2003)

    Google Scholar 

  16. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)

    MATH  Google Scholar 

  17. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of DAC 2001, pp. 530–535. ACM, New York (2001)

    Google Scholar 

  18. Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Knuth, D.: The Art of Computer Programming. Sorting and Searching, vol. 3. Addison-Wesley, Reading (1997)

    MATH  Google Scholar 

  20. Bellman, R.E.: On a Routing Problem. Quarterly of applied mathematics 16, 87–90 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  21. Ford, L.R., Fulkerson, D.R.: Flows in Networks. Princeton University Press, Princeton (1962)

    MATH  Google Scholar 

  22. Prim, R.C.: Shortest Connection Networks and Some Generalisations. Bell System Technical Journal 36, 1389–1401 (1957)

    Article  Google Scholar 

  23. Stump, A., Barrett, C.W., Dill, D.L.: CVC: A Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234–245. ACM Press, New York (2002)

    Chapter  Google Scholar 

  25. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453–457 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  26. Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. Technical Report 148, HP Labs (2003)

    Google Scholar 

  27. Leino, K.R.M., Millstein, T.D., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55, 209–226 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  28. Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  29. Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  30. Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: Proceedings of ICSE 2003, pp. 385–395. IEEE Computer Society Press, Los Alamitos (2003)

    Google Scholar 

  31. Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Palsberg, J., Abadi, M. (eds.) Proceedings of POPL 2005, pp. 351–363. ACM Press, New York (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Artificial Intelligence Laboratory, DIST, Università degli Studi di Genova, Viale F. Causa 13, 16145, Genova, Italy

    Alessandro Armando, Jacopo Mantovani & Lorenzo Platania

Authors
  1. Alessandro Armando
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacopo Mantovani
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lorenzo Platania
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Software Systems, Tampere University of Technology, PO Box 553, FI-33101, Tampere, Finland

    Antti Valmari

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Armando, A., Mantovani, J., Platania, L. (2006). Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_9

Download citation

  • DOI: https://doi.org/10.1007/11691617_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-33102-5

  • Online ISBN: 978-3-540-33103-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation