Automated verification of pointer programs in pointer logic |
| |
Authors: | Zhifang WANG Yiyun CHEN Zhenming WANG Baojian HUA |
| |
Affiliation: | (1) Department of Computer Science and Technology, University of Science and Technology of China, Hefei, 230026, China;(2) Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, 215123, 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. |
| |
Keywords: | software safety pointer logic alias analysis automated verification |
本文献已被 万方数据 SpringerLink 等数据库收录! |
|