An Eztension to Pointer Logic for Verification
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..
Zhifang Wang Yiyun Chen Zhenming Wang Wei Wang Bo Tian
Department of Computer Science and Technology, University of Science and Technology of China Hefei, 230026, China Suzhou Institute for Advanced Study, University of Science and Technology of China Suzhou, 215123, China
国际会议
南京
英文
49-56
2008-06-17（万方平台首次上网日期，不代表论文的发表时间）