Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2007)

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

Abstract

Research on the automatic verification of heap-manipulating programs (HMPs) — programs that manipulate unbounded linked data structures via pointers — has blossomed recently, with many different approaches all showing leaps in performance and expressiveness. A year ago, we proposed a small logic for specifying predicates about HMPs and demonstrated that an inference-rule-based decision procedure could be performance-competitive, and in many cases superior to other methods known at the time. That work, however, was a proof-of-concept, with a logic fragment too small to verify most real programs. In this work, we generalize our previous results to be practically useful: we allow the data in heap nodes to be mutable, we allow more than a single pointer field, and we add new primitives needed to verify cyclic structures. Each of these extensions necessitates new or changed inference rules, with the concomitant changes to the proofs and decision procedure. Yet, our new decision procedure, with the more general logic, actually runs as fast as our previous results. With these generalizations, we can automatically verify many more HMP examples, including three small container functions from the Linux kernel.

This work was supported by a research grant from the Natural Sciences and Engineering Research Council of Canada and a University of British Columbia Graduate Fellowship.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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.

Similar content being viewed by others

References

  1. 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, Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Bingham, J., Rakamarić, Z.: A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, UBC Dept. Comp. Sci. Tech Report TR-2005-19 (2005), http://www.cs.ubc.ca/cgi-bin/tr/2005/TR-2005-19

  3. Rakamarić, Z., Bingham, J., Hu, A.J.: 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

  4. Gotsman, A., Berdine, J., Cook, B.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Berdine, J., Calcagno, C., O’Hearn, P.W.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, Springer, Heidelberg (2004)

    Google Scholar 

  6. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: Intl. Symp. on Formal Methods for Components and Objects, FMCO (2006)

    Google Scholar 

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

  8. Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Symp. on Principles of Programming Languages, POPL (2002)

    Google Scholar 

  9. Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University (1979)

    Google Scholar 

  10. Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Symp. on Principles of Programming Languages, POPL (1983)

    Google Scholar 

  11. Benedikt, M., Reps, T., Sagiv, M.: A Decidable Logic for Describing Linked Data Structures. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol. 1576, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Immerman, N., et al.: The Boundary Between Decidability and Undecidability for Transitive Closure Logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, Springer, Heidelberg (2004)

    Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Symp. on Principles of Programming Languages, POPL (1977)

    Google Scholar 

  14. Dams, D., Namjoshi, K.S.: Shape Analysis Through Predicate Abstraction and Model Checking. In: Zuck, L.D., et al. (eds.) VMCAI 2003. LNCS, vol. 2575, Springer, Heidelberg (2002)

    Google Scholar 

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

  16. Das, S., Dill, D.L., Park, S.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Symp. on Principles of Programming Languages, POPL (2002)

    Google Scholar 

  18. Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Conf. on Programming Language Design and Implementation, PLDI (2001)

    Google Scholar 

  19. Wies, T., et al.: Field Constraint Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Reps, T., Sagiv, M., Loginov, A.: Finite Differencing of Logical Formulas for Static Analysis. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Yorsh, G., et al.: A Logic of Reachable Patterns in Linked Data-Structures. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Immerman, N., et al.: Verification via Structure Simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, Springer, Heidelberg (2004)

    Google Scholar 

  23. Lahiri, S.K., Qadeer, S.: Verifying Properties of Well-Founded Linked Lists. In: Symp. on Principles of Programming Languages, POPL (2006)

    Google Scholar 

  24. Manevich, R., et al.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)

    Google Scholar 

  25. Loginov, A., Reps, T.W., Sagiv, S.: Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, Springer, Heidelberg (2005)

    Google Scholar 

  26. Distefano, D., O’Hearn, P.W., Yang, H.: A Local Shape Analysis Based on Separation Logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Ishtiaq, S., O’Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: Symp. on Principles of Programming Languages, POPL (2001)

    Google Scholar 

  28. Magill, S., Nanevski, A., Clarke, E.M., Lee, P.: Inferring Invariants in Separation Logic for Imperative List-processing Programs. In: Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, SPACE (2006)

    Google Scholar 

  29. Lev-Ami, T., Immerman, N., Sagiv, M.: Abstraction for Shape Analysis with Fast and Precise Transformers. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA Implementation Secrets. In: Conf. on Implementation and Application of Automata, CIAA (2000)

    Google Scholar 

  31. Lev-Ami, T., Sagiv, M.: TVLA: A System for Implementing Static Analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, Springer, Heidelberg (2000)

    Google Scholar 

  32. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: Conf. on Programming Language Design and Implementation, PLDI (2001)

    Google Scholar 

  33. Yorsh, G., Reps, T., Sagiv, M.: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, Springer, Heidelberg (2004)

    Google Scholar 

  34. Ranise, S., Zarba, C.G.: A Theory of Singly-Linked Lists and its Extensible Decision Procedure. In: IEEE Int. Conf. on Software Engineering and Formal Methods, SEFM (2006)

    Google Scholar 

  35. McMillan, K.L.: Applications of Craig Interpolants in Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)

    Google Scholar 

  36. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–583 (1969)

    Article  MATH  Google Scholar 

  37. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  38. Lev-Ami, T., et al.: Simulating Reachability using First-Order Logic with Applications to Verification of Linked Data Structures. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Zvonimir Rakamarić & Alan J. Hu

  2. Intel Corporation, Hillsboro, Oregon, USA

    Jesse Bingham

Authors
  1. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jesse Bingham
    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

Editor information

Byron Cook Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rakamarić, Z., Bingham, J., Hu, A.J. (2007). 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) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69738-1_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69735-0

  • Online ISBN: 978-3-540-69738-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation