loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
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.