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.
|Title of host publication||Verification, Model Checking, and Abstract Interpretation|
|Editors||Byron Cook, Andreas Podelski|
|Publisher||Springer Berlin Heidelberg|
|Publication status||Published - 2007|
|Event||8th International Conference on Verification, Model Checking, and Abstract Interpretation - Nice, France|
Duration: 14 Jan 2007 → 16 Jan 2007
Conference number: 8
|Conference||8th International Conference on Verification, Model Checking, and Abstract Interpretation|
|Abbreviated title||VMCAI 2007|
|Period||14/01/07 → 16/01/07|
Bibliographical noteAuthor can archive post-print (ie final draft post-refereeing).
Nguyen, H. H., David, C., Qin, S., & Chin, W-N. (2007). Automated Verification of Shape and Size Properties Via Separation Logic. In B. Cook, & A. Podelski (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 251-266). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_18