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

Automated verification of pointer programs in pointer logic

  • Research Article
  • Published:
Frontiers of Computer Science in China Aims and scope Submit manuscript

Abstract

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic-Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool-plcc was implemented to automatically verify a number of non-trivial pointer programs.

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

Access this article

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

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. O’Hearn P, Reynolds J, Yang H. Local reasoning about programs that alter data structures. In: Proceedings of the 15th International Workshop on Computer Science Logic. London: Springer, 2001, 1–19

    Google Scholar 

  2. Reynolds J. Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington: IEEE Computer Society, 2002, 55–74

    Chapter  Google Scholar 

  3. Jonkers H B M. Abstract storage structures. In: de Bakker, van. Vllet, eds. Algorithmic Languages. 1981, 321–343

  4. Deutsch A. A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. In: Proceedings of the 1992 International Conference on Computer Languages. California: IEEE Computer Society, 1992, 2–13

    Chapter  Google Scholar 

  5. Venet A. Automatic analysis of pointer aliasing for untyped programs. Science of Computer Programming. 1999, 35(2):223–248

    Article  MATH  MathSciNet  Google Scholar 

  6. Bozga M, Iosif R, Laknech Y. Storeless semantics and alias logic. In: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation. New York: ACM Press, 2003, 55–65

    Chapter  Google Scholar 

  7. Rinetzky N, Bauer J, Reps T, et al. A semantics for procedure local heaps and its abstractions. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 2005, 296–309

    Google Scholar 

  8. Chen Y, Ge L, Hua B, et al. Design of a certifying compiler supporting proof of program safety. In: Proceedings of the 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering. Washington: IEEE Computer Society, 2007, 117–126

    Google Scholar 

  9. Chen Y, Ge L, Hua B, et al. A pointer logic and certifying compiler. Frontiers of Computer Science in China. 2007, 1(3):297–312

    Article  Google Scholar 

  10. Deutsch A. Interprocedural may-alias analysis for pointers: beyond k-limiting. In: Proceedings of the ACM SIGPLAN’94 Conference on Programing language Design and Implementation. New York: ACM Press, 1994, 230–241

    Google Scholar 

  11. Bornat R. Proving pointer programs in hoare logic. In: Proceedings of the 5th International Conference on Mathematics of Program Construction. London: Springer, 2000, 102–126

    Google Scholar 

  12. Topor R. The correctness of the Schorr-Waite list marking algorithm. Acta Informatica. 1979, 11: 211–221

    Article  MATH  MathSciNet  Google Scholar 

  13. Yang H. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Henglein F, Hughes J, Makholm H, et al. eds. SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. IT University of Copenhagen, 2001, 41–68

  14. Mehta F, Nipkow T. Proving pointer programs in higherorder logic. Information and Computation. 2005, 199(1–2): 200–227

    Article  MATH  MathSciNet  Google Scholar 

  15. Hubert T, Marché C. A case study of C source code verification: the Schorr-Waite algorithm. In: Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods. Washington: IEEE Computer Society, 2005, 190–199

    Chapter  Google Scholar 

  16. Nipkow T, Paulson L, Wenzel M. Isabelle/HOL: A proof assistant for higher-order logic. Computer Science. London: Springer, 2002, 259–278

    Google Scholar 

  17. Bornat R, Sufrin B. Animating formal proofs at the surface: the Jape proof calculator. The Computer Journal. 1999, 43: 177–192

    Article  Google Scholar 

  18. Loginov A, Reps T, Sagiv M. Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Proceedings of the 13th International Static Analysis Symposium. London: Springer, 2006, 261–279

    Google Scholar 

  19. Cooper D C. Theorem proving in arithmetic without multiplication. In: Meltzer B, Michie D, eds, Machine Intelligence. 1972, 91–100

  20. Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM. 1969, 12(10): 576–583

    Article  MATH  Google Scholar 

  21. Hoare C A R, He J. A trace model for pointers and objects. In: Proceedings of the 13th European Conference on Object-Oriented Programming. London: Springer-Verlag, 1999, 1–17

    Google Scholar 

  22. Lahiri S K, Qadeer S. Verifying properties of well-founded linked lists. In: Proceedings of the 33th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2006, 115–126

    Google Scholar 

  23. Chatterjee S, Lahiri S K, Qadeer S, et al. A reachability predicate for analyzing low-level software. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. London: Springer, 2007, 19–33

    Chapter  Google Scholar 

  24. Lahiri S K, Qadeer S. Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2008, 171–182

    Chapter  Google Scholar 

  25. Møeller A, Schwartzbach M I. The pointer assertion logic engine. In: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation. New York: ACM Press, 2001, 221–231

    Chapter  Google Scholar 

  26. Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems. 2002, 24(3): 217–298

    Article  Google Scholar 

  27. Walker D, Morrisett G. Alias types for recursive data structures. In: Selected papers from the 3rd International Workshop on Types in Compilation. London: Springer-Verlag, 2001, 177–206

    Google Scholar 

  28. Xi H. Applied type system (extended abstract). In: the postworkshop proceedings of TYPES 2003. Berlin: Springer, 2004, 394–408

    Google Scholar 

  29. Chen C, Xi H. Combining programming with theorem proving. In: Proceedings of the 10thACM SIGPLAN international conference on Functional programming. New York: ACM press, 2005, 66–77

    Google Scholar 

  30. Berdine J, Calcagno C, O’Hearn P W. Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th International Symposium on Formal Methods for Components and Objects. London: Springer, 2005, 115–137

    Google Scholar 

  31. Ireland A. Towards Automatic Assertion Refinement for Separation Logic. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering. Washington: IEEE Computer Society, 2006, 309–312

    Chapter  Google Scholar 

  32. Nguyen H H, David C, Qin S, et al. Automated verification of shape and size properties via separation logic. In: Proceedings of eighth International Conference on Verification, Model Checking and Abstract Interpretation. Berlin: Springer, 2007, 251–266

    Chapter  Google Scholar 

  33. Berdine J, Calcagno C, O’Hearn P W. Symbolic execution with separation logic. In: Proceedings of the 3rd Asian Symposium on Programming Languages and Systems. London: Springer-Verlag, 2005, 52–68

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Technology, University of Science and Technology of China, Hefei, 230026, China

    Zhifang Wang, Yiyun Chen, Zhenming Wang & Baojian Hua

Authors
  1. Zhifang Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yiyun Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhenming Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Baojian Hua
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhifang Wang.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wang, Z., Chen, Y., Wang, Z. et al. Automated verification of pointer programs in pointer logic. Front. Comput. Sci. China 2, 380–397 (2008). https://doi.org/10.1007/s11704-008-0033-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11704-008-0033-8

Keywords

Search

Navigation