Automated Verification of Shape and Size Properties via Separation Logic

Nguyen, H.-H.; David, C.; Qin, S.; Chin, W.-N.; Cook, B.; Podelski, A.

doi:10.1007/978-3-540-69738-1_18

Automated Verification of Shape and Size Properties via Separation Logic

Nguyen, H.-H.; David, C.; Qin, S.; Chin, W.-N.; Cook, B.; Podelski, A.

Authors

H.-H. Nguyen

C. David

S. Qin

W.-N. Chin

B. Cook

A. Podelski

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.

Citation

Nguyen, H., David, C., Qin, S., Chin, W., Cook, B., & Podelski, A. (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) (251-266). https://doi.org/10.1007/978-3-540-69738-1_18

Conference Name	Eighth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007)
Conference Location	Nice, France
Start Date	Jan 14, 2007
End Date	Jan 16, 2007
Publication Date	Jan 1, 2007
Deposit Date	Nov 16, 2009
Publicly Available Date	Dec 10, 2009
Publisher	Springer Verlag
Pages	251-266
Series Title	Lecture notes in computer science
Series Number	4349
Book Title	Proceeding of the 8th international conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007).
ISBN	9783540697350
DOI	https://doi.org/10.1007/978-3-540-69738-1_18