Cookies

We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.


Durham Research Online
You are in:

Automated verification of shape and size properties via separation logic.

Nguyen, H. H. and David, C. and Qin, S. and Chin, W.-N. (2007) 'Automated verification of shape and size properties via separation logic.', in Proceeding of the 8th international conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007). Berlin: Springer, pp. 251-266. Lecture notes in computer science. (4349).

Abstract

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise and expressive for ensuring the safety of pointer-based programs. Our approach uses user-definable shape predicates to allow programmers to describe a wide range of data structures with their associated size properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded inductive predicates using unfold/fold reasoning. We have proven the soundness and termination of our verification system, and have built a prototype system.

Item Type:Book chapter
Full text:PDF - Accepted Version (272Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/978-3-540-69738-1_18
Publisher statement:The original publication is available at www.springerlink.com
Record Created:16 Nov 2009 16:35
Last Modified:29 Nov 2011 16:59

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Usage statisticsLook up in GoogleScholar | Find in a UK Library