|
|
|
Automated verification of pointer programs in
pointer logic |
| WANG Zhifang, CHEN Yiyun, WANG Zhenming, HUA Baojian |
| Department of Computer Science and Technology, University of Science and Technology of China；Suzhou Institute for Advanced Study, University of Science and Technology of China; |
|
|
|
|
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.
|
|
Issue Date: 05 December 2008
|
|
| 1 |
O'Hearn P, Reynolds J, Yang H . Local reasoning about programs that alter data structures. In: Proceedings of the 15th International Workshopon Computer Science Logic. London: Springer, 2001, 1–19
|
| 2 |
Reynolds J . Separationlogic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in ComputerScience. Washington: IEEE Computer Society, 2002, 55–74
|
| 3 |
Jonkers H B M . Abstract storage structures. In: de Bakker, van. Vllet, eds. Algorithmic Languages. 1981, 321–343
|
| 4 |
Deutsch A . Astoreless model of aliasing and its abstractions using finite representationsof right-regular equivalence relations. In: Proceedings of the 1992 International Conference on Computer Languages. California: IEEE Computer Society, 1992, 2–13
|
| 5 |
Venet A . Automaticanalysis of pointer aliasing for untyped programs. Science of Computer Programming. 1999, 35(2):223–248.
doi:10.1016/S0167-6423(99)00012-X
|
| 6 |
Bozga M, Iosif R, Laknech Y . Storeless semantics and alias logic. In: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluationand semantics-based program manipulation. New York: ACM Press, 2003, 55–65
|
| 7 |
Rinetzky N, Bauer J, Reps T, et al.. A semantics for procedure local heaps and itsabstractions. In: Proceedings of the 32ndACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 2005, 296–309
|
| 8 |
Chen Y, Ge L, Hua B, et al.. Design of a certifying compiler supporting proofof program safety. In: Proceedings of the1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering. Washington: IEEE Computer Society, 2007, 117–126
|
| 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.
doi:10.1007/s11704-007-0029-9
|
| 10 |
Deutsch A . Interproceduralmay-alias analysis for pointers: beyond k-limiting. In: Proceedings of the ACMSIGPLAN'94 Conference on Programing language Design and Implementation. New York: ACM Press, 1994, 230–241
|
| 11 |
Bornat R . Provingpointer programs in hoare logic. In: Proceedingsof the 5th International Conference on Mathematics of Program Construction. London: Springer, 2000, 102–126
|
| 12 |
Topor R . Thecorrectness of the Schorr-Waite list marking algorithm. Acta Informatica. 1979, 11: 211–221.
doi:10.1007/BF00289067
|
| 13 |
Yang H . Anexample of local reasoning in BI pointer logic: the Schorr-Waite graphmarking algorithm. In: Henglein F, Hughes J, MakholmH, et al.. eds. SPACE 2001: InformalProceedings of Workshop on Semantics, Program Analysis and ComputingEnvironments for Memory Management. IT University of Copenhagen, 2001, 41–68
|
| 14 |
Mehta F, Nipkow T . Proving pointer programsin higher-order logic. Information andComputation. 2005, 199(1–2): 200–227.
doi:10.1016/j.ic.2004.10.007
|
| 15 |
Hubert T, Marché C . A case study of C sourcecode verification: the Schorr-Waite algorithm. In: Proceedings of the 3rd IEEE International Conference on SoftwareEngineering and Formal Methods. Washington: IEEE Computer Society, 2005, 190–199
|
| 16 |
Nipkow T, Paulson L, Wenzel M . Isabelle/HOL: A proof assistant for higher-order logic. Computer Science. London: Springer, 2002, 259–278
|
| 17 |
Bornat R, Sufrin B . Animating formal proofs atthe surface: the Jape proof calculator. The Computer Journal. 1999, 43: 177–192.
doi:10.1093/comjnl/42.3.177
|
| 18 |
Loginov A, Reps T, Sagiv M . Automated verification of the Deutsch-Schorr-Waite tree-traversalalgorithm. In: Proceedings of the 13thInternational Static Analysis Symposium. London: Springer, 2006, 261–279
|
| 19 |
Cooper D C . Theorem proving in arithmetic without multiplication.In: Meltzer B, MichieD, 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.
doi:10.1145/363235.363259
|
| 21 |
Hoare C A R, He J . A trace model for pointersand objects. In: Proceedings of the 13thEuropean Conference on Object-Oriented Programming. London: Springer-Verlag, 1999, 1–17
|
| 22 |
Lahiri S K, Qadeer S . Verifying properties of well-foundedlinked lists. In: Proceedings of the 33thannual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2006, 115–126
|
| 23 |
Chatterjee S, Lahiri S K, Qadeer S, et al.. A reachability predicate for analyzing low-levelsoftware. In: Proceedings of the 13th InternationalConference on Tools and Algorithms for the Construction and Analysisof Systems. London: Springer, 2007, 19–33
|
| 24 |
Lahiri S K, Qadeer S . Back to the future: revisitingprecise program verification using SMT solvers. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principlesof programming languages. NewYork: ACM press, 2008, 171–182
|
| 25 |
Møeller A, Schwartzbach M I . The pointer assertion logicengine. In: Proceedings of the ACM SIGPLAN2001 conference on Programming language design and implementation. New York: ACM Press, 2001, 221–231
|
| 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.
doi:10.1145/514188.514190
|
| 27 |
Walker D, Morrisett G . Alias types for recursivedata structures. In: Selected papers fromthe 3rd International Workshop on Types in Compilation. London: Springer-Verlag, 2001, 177–206
|
| 28 |
Xi H . Appliedtype system (extended abstract). In: thepost-workshop proceedings of TYPES 2003. Berlin: Springer, 2004, 394–408
|
| 29 |
Chen C, Xi H . Combining programming withtheorem proving. In: Proceedings of the10th ACM SIGPLAN international conference on Functional programming. New York: ACM press, 2005, 66–77
|
| 30 |
Berdine J, Calcagno C, O'Hearn P W . Smallfoot: modular automatic assertion checking withseparation logic. In: Proceedings of the4th International Symposium on Formal Methods for Components and Objects. London: Springer, 2005, 115–137
|
| 31 |
Ireland A . TowardsAutomatic Assertion Refinement for Separation Logic. In: Proceedings of the 21st IEEE/ACM International Conference on AutomatedSoftware Engineering. Washington: IEEE Computer Society, 2006, 309–312
|
| 32 |
Nguyen H H, David C, Qin S, et al.. Automated verification of shape and size propertiesvia separation logic. In: Proceedings ofeighth International Conference on Verification, Model Checking andAbstract Interpretation. Berlin: Springer, 2007, 251–266
|
| 33 |
Berdine J, Calcagno C, O'Hearn P W . Symbolic execution with separation logic.In: Proceedings of the 3rd Asian Symposium on ProgrammingLanguages and Systems. London: Springer-Verlag, 2005, 52–68
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
