2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering An Extension to Pointer Logic for Verification June 17-June 19 ISBN: 978-0-7695-3249-3
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2008.13
The safety of pointer programs is an important issue in high-assurance software design, and their verification remains a major challenge. Pointer Logic has been proposed to verify basic safety properties of pointer programs in our previous work, but still lacks support for a wide range of pointer programs. In this work, we present an extension to Pointer Logic by: 1) introducing modular reasoning to scale better on programs involving function calls; 2) allowing pointer arithmetic to take more advantage of pointers in programming. Moreover, to demonstrate that Pointer Logic is a useful approach to verification, we implement a tool - plcc to automatically verify a range of non-trivial programs, including basic operations on singly-linked lists, trees, circular doubly-linked list, dynamic arrays etc.
Citation:
Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang, Bo Tian, "An Extension to Pointer Logic for Verification," tase, pp.49-56, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||