Advertisement

Automated Verification of Shape and Size Properties Via Separation Logic

  • Huu Hai Nguyen
  • Cristina David
  • Shengchao Qin
  • Wei-Ngan Chin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system.

Keywords

Automate Reasoning Size Property Disjunctive Normal Form Data Node Separation Logic 
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.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., et al. (eds.) FMCO 2005. LNCS, vol. 4111, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Bingham, J., Rakamaric, 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)CrossRefGoogle Scholar
  4. 4.
    Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of ACM 24(1), 44–67 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ACM SIGPLAN ICFP, Tallinn, Estonia (September 2005)Google Scholar
  6. 6.
    Chin, W.N., Khoo, S.C.: Calculating sized types. In: ACM SIGPLAN PEPM, pp. 62–72, Boston, United States (January 2000)Google Scholar
  7. 7.
    Chin, W.N., Khoo, S.C., Qin, S.C., Popeea, C., Nguyen, H.H.: Verifying Safety Policies with Size Properties and Alias Controls. In: ACM SIGSOFT ICSE, St. Louis, Missouri (May 2005)Google Scholar
  8. 8.
    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
  9. 9.
    Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: ACM POPL, pp. 410–423. ACM Press, New York (1996)Google Scholar
  10. 10.
    Isthiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, London (January 2001)Google Scholar
  11. 11.
    Jia, L., Walker, D.: ILC: A foundation for automated reasoning about pointer programs. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)Google Scholar
  13. 13.
    Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: ACM POPL, pp. 247–258 (2005)Google Scholar
  14. 14.
    Moeller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: ACM PLDI, (June 2001)Google Scholar
  15. 15.
    Nguyen, H.H., et al.: Automated Verification of Shape and Size Properties via Separation Logic. Technical report, SoC, Natl Univ. of Singapore (July 2006), available at http://www.comp.nus.edu.sg/~nguyenh2/papers/vmcai07-report.pdf
  16. 16.
    Pugh, W.: The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM 8, 102–114 (1992)CrossRefGoogle Scholar
  17. 17.
    Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: IEEE LICS, Copenhagen, Denmark (July 2002)Google Scholar
  18. 18.
    Rugina, R.: Quantitative Shape Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)Google Scholar
  19. 19.
    Sagiv, S., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3) (2002)Google Scholar
  20. 20.
    Sims, É.-J.: Extending separation logic with fixpoints and postponed substitution. Theoretical Computer Science 351(2), 258–275 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Walker, D., Morrisett, G.: Alias Types for Recursive Data Structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 177–206. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Huu Hai Nguyen
    • 1
  • Cristina David
    • 2
  • Shengchao Qin
    • 3
  • Wei-Ngan Chin
    • 1
    • 2
  1. 1.Computer Science Programme, Singapore-MIT Alliance 
  2. 2.Department of Computer Science, National University ofSingapore
  3. 3.Department of Computer Science, Durham University 

Personalised recommendations