Skip to main content
SpringerLink
Log in

Verifying Heap-Manipulating Programs in an SMT Framework

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4762))

Abstract

Automated software verification has made great progress recently, and a key enabler of this progress has been the advances in efficient, automated decision procedures suitable for verification (Boolean satisfiability solvers and satisfiability-modulo-theories (SMT) solvers). Verifying general software, however, requires reasoning about unbounded, linked, heap-allocated data structures, which in turn motivates the need for a logical theory for such structures that includes unbounded reachability. So far, none of the available SMT solvers supports such a theory. In this paper, we present our integration of a decision procedure that supports unbounded heap reachability into an available SMT solver. Using the extended SMT solver, we can efficiently verify examples of heap-manipulating programs that we could not verify before.

Supported by (1) a research grant from the Natural Sciences and Engineering Research Council of Canada, (2) a University of British Columbia Graduate Fellowship, (3) ORCHID, a project sponsored by Provincia Autonoma di Trento, and (4) a research grant from Intel.

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. Ackermann, W.: Solvable Cases of the Decision Problem. In: Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam (1954)

    Google Scholar 

  2. Babić, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 366–378. Springer, Heidelberg (2007)

    Google Scholar 

  3. Balaban, I., Pnueli, A., Zuck, L.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)

    Google Scholar 

  4. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 203–213 (2001)

    Google Scholar 

  5. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)

    Google Scholar 

  6. Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, Springer, Heidelberg (1999)

    Google Scholar 

  7. Beyer, D., Henzinger, T.A., Théoduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 532–546. Springer, Heidelberg (2006)

    Google Scholar 

  8. Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007)

    Google Scholar 

  9. Bingham, J., Rakamarić, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 207–221. Springer, Heidelberg (2005)

    Google Scholar 

  10. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Ranise, S., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 335–349. Springer, Heidelberg (2005)

    Google Scholar 

  11. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Ranise, S., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation 204, 1493–1525 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  12. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Schulz, S., Sebastiani, R.: The MathSAT 3 system. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 315–321. Springer, Heidelberg (2005)

    Google Scholar 

  13. Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 527–541. Springer, Heidelberg (2006)

    Google Scholar 

  14. Charlton, N., Huth, M.: Hector: Software model checking with cooperating analysis plugins. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 168–172. Springer, Heidelberg (2007)

    Google Scholar 

  15. Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)

    Google Scholar 

  16. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design 25(2-3), 105–127 (2004)

    Article  MATH  Google Scholar 

  17. Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking, Technical Report HPL-2003-148, HP Labs, Palo Alto, CA (2003)

    Google Scholar 

  18. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 234–245 (2002)

    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. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL. Symp. on Principles of Programming Languages, pp. 58–70 (2002)

    Google Scholar 

  21. Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)

    Google Scholar 

  22. Ivančić, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: ICCD. Intl. Conf. on Computer Design, pp. 297–308 (2005)

    Google Scholar 

  23. Jensen, J.L., Jørgensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 226–236 (1997)

    Google Scholar 

  24. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, Springer, Heidelberg (2001)

    Google Scholar 

  25. Krstić, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 602–617. Springer, Heidelberg (2007)

    Google Scholar 

  26. Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 413–426. Springer, Heidelberg (2006)

    Google Scholar 

  27. Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL. Symp. on Principles of Programming Languages, pp. 115–126 (2006)

    Google Scholar 

  28. Lahiri, S.K., Qadeer, S.: A decision procedure for well-founded reachability, Microsoft Research Tech Report MSR-TR-2007-43 (2007)

    Google Scholar 

  29. Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005)

    Google Scholar 

  30. Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000)

    Google Scholar 

  31. Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)

    Google Scholar 

  32. Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 381–422. Springer, Heidelberg (2003)

    Google Scholar 

  33. McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 476–490. Springer, Heidelberg (2005)

    Google Scholar 

  34. Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI. Conf. on Programming Language Design and Implementation, pp. 221–231 (2001)

    Google Scholar 

  35. Nelson, G.: Techniques for program verification. PhD thesis, Stanford University (1979)

    Google Scholar 

  36. Nelson, G.: Verifying reachability invariants of linked structures. In: POPL. Symp. on Principles of Programming Languages, pp. 38–47 (1983)

    Google Scholar 

  37. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  38. Rakamarić, Z., Bingham, J., Hu, A.: A better logic and decision procedure for predicate abstraction of heap-manipulating programs, UBC Dept. Comp. Sci. Tech Report TR-2006-02 (2006), http://www.cs.ubc.ca/cgi-bin/tr/2006/TR-2006-02

  39. Rakamarić, Z., Bingham, J., Hu, A.J.: An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 106–121. Springer, Heidelberg (2007)

    Google Scholar 

  40. Ranise, S., Zarba, C.G.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM. IEEE Intl. Conf. on Software Engineering and Formal Methods (2006)

    Google Scholar 

  41. Yorsh, G., Rabinovich, A., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, Springer, Heidelberg (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ITC-IRST, Povo, Trento, Italy

    Roberto Bruttomesso & Alessandro Cimatti

  2. Department of Computer Science, University of British Columbia, Canada

    Zvonimir Rakamarić & Alan J. Hu

Authors
  1. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roberto Bruttomesso
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alan J. Hu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alessandro Cimatti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Kedar S. Namjoshi Tomohiro Yoneda Teruo Higashino Yoshio Okamura

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rakamarić, Z., Bruttomesso, R., Hu, A.J., Cimatti, A. (2007). Verifying Heap-Manipulating Programs in an SMT Framework . In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds) Automated Technology for Verification and Analysis. ATVA 2007. Lecture Notes in Computer Science, vol 4762. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75596-8_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-75596-8_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-75595-1

  • Online ISBN: 978-3-540-75596-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation