Automated Verification of Shape and Size Properties Via Separation Logic

Huu Hai Nguyen; Cristina David; Shengchao Qin; Wei-Ngan Chin

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

Automated Verification of Shape and Size Properties Via Separation Logic

Huu Hai Nguyen
, Cristina David
, Shengchao Qin
, Wei-Ngan Chin

SCEDT School Executive Team

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

252 Downloads (Pure)

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.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation
Editors	Byron Cook, Andreas Podelski
Publisher	Springer Berlin Heidelberg
Pages	251-266
ISBN (Print)	978-3-540-69735-0
DOIs	https://doi.org/10.1007/978-3-540-69738-1_18
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

Conference	8th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated title	VMCAI 2007
Country/Territory	France
City	Nice
Period	14/01/07 → 16/01/07

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).

Access to Document

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

Full textFinal published version, 242 KBLicence: CC BY-NC-ND

http://link.springer.com/10.1007/978-3-540-69738-1_18

Cite this

@inproceedings{cff7853e27c7453abf0452de4772ef56,

title = "Automated Verification of Shape and Size Properties Via Separation Logic",

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.",

author = "Nguyen, \{Huu Hai\} and Cristina David and Shengchao Qin and Wei-Ngan Chin",

note = "Author can archive post-print (ie final draft post-refereeing). ; 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007 ; Conference date: 14-01-2007 Through 16-01-2007",

year = "2007",

doi = "10.1007/978-3-540-69738-1\_18",

language = "English",

isbn = "978-3-540-69735-0",

pages = "251--266",

editor = "Byron Cook and Andreas Podelski",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

publisher = "Springer Berlin Heidelberg",

}

Nguyen, HH, 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. Springer Berlin Heidelberg, pp. 251-266, 8th International Conference on Verification, Model Checking, and Abstract Interpretation, Nice, France, 14/01/07. https://doi.org/10.1007/978-3-540-69738-1_18

TY - GEN

T1 - Automated Verification of Shape and Size Properties Via Separation Logic

AU - Nguyen, Huu Hai

AU - David, Cristina

AU - Qin, Shengchao

AU - Chin, Wei-Ngan

N1 - Conference code: 8

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-69738-1_18

DO - 10.1007/978-3-540-69738-1_18

M3 - Conference contribution

SN - 978-3-540-69735-0

SP - 251

EP - 266

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Cook, Byron

A2 - Podelski, Andreas

PB - Springer Berlin Heidelberg

T2 - 8th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 14 January 2007 through 16 January 2007

ER -

Automated Verification of Shape and Size Properties Via Separation Logic

Abstract

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this