Automated verification of shape, size and bag properties via user-defined predicates in separation logic

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

Research output: Contribution to journalArticle

110 Downloads (Pure)

Abstract

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this paper, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach.
Original languageEnglish
Pages (from-to)1006-1036
JournalScience of Computer Programming
Volume77
Issue number9
DOIs
Publication statusPublished - Aug 2012

Bibliographical note

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

Fingerprint Dive into the research topics of 'Automated verification of shape, size and bag properties via user-defined predicates in separation logic'. Together they form a unique fingerprint.

  • Cite this