An Extension 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

• Type: Journal
• Year: 2008
• Where: TASE
• Authors: Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang, Bo Tian
• Keywords: Basic Safety Properties, Pointer Logic, Pointer Programs, Software Engineering, TASE 2008