Advertisement

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

  • Zvonimir Rakamarić
  • Jesse Bingham
  • Alan J. Hu
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Model Check Inference Rule Decision Procedure Separation Logic Predicate Abstraction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)CrossRefGoogle Scholar
  2. 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. 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. 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)CrossRefGoogle Scholar
  5. 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. 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. 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. 8.
    Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Symp. on Principles of Programming Languages, POPL (2002)Google Scholar
  9. 9.
    Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University (1979)Google Scholar
  10. 10.
    Nelson, G.: Verifying Reachability Invariants of Linked Structures. In: Symp. on Principles of Programming Languages, POPL (1983)Google Scholar
  11. 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)CrossRefGoogle Scholar
  12. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  17. 17.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Symp. on Principles of Programming Languages, POPL (2002)Google Scholar
  18. 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. 19.
    Wies, T., et al.: Field Constraint Analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 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)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  27. 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. 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. 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)CrossRefGoogle Scholar
  30. 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. 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. 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. 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. 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. 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. 36.
    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–583 (1969)zbMATHCrossRefGoogle Scholar
  37. 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)zbMATHCrossRefGoogle Scholar
  38. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Zvonimir Rakamarić
    • 1
  • Jesse Bingham
    • 2
  • Alan J. Hu
    • 1
  1. 1.Department of Computer Science, University of British ColumbiaCanada
  2. 2.Intel Corporation, Hillsboro, OregonUSA

Personalised recommendations