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).
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:||(AM) Accepted Manuscript|
Download PDF (272Kb)
|Publisher Web site:||http://dx.doi.org/10.1007/978-3-540-69738-1_18|
|Publisher statement:||The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-540-69738-1_18|
|Record Created:||16 Nov 2009 16:35|
|Last Modified:||31 Mar 2015 12:56|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|