Automated Verification of Shape and Size Properties Via Separation Logic

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

194 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 languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
EditorsByron Cook, Andreas Podelski
PublisherSpringer Berlin Heidelberg
Pages251-266
ISBN (Print)978-3-540-69735-0
DOIs
Publication statusPublished - 2007
Event8th International Conference on Verification, Model Checking, and Abstract Interpretation - Nice, France
Duration: 14 Jan 200716 Jan 2007
Conference number: 8

Conference

Conference8th International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI 2007
CountryFrance
CityNice
Period14/01/0716/01/07

Bibliographical note

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

Fingerprint Dive into the research topics of 'Automated Verification of Shape and Size Properties Via Separation Logic'. Together they form a unique fingerprint.

  • Cite this

    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