Lightweight support for magic wands in an automatic verifier
OPEN ACCESS
Author / Producer
Date
2014
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Permission-based verication logics such as separation logic have led to the development of many practical verication tools over the last decade. Veriers employ the separating conjunction A B to elegantly handle aliasing problems, framing, race conditions, etc. Introduced along with the separating conjunction, the magic wand connective, written A − B, can describe hypothetical modications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verication tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, particularly for specifying loop invariants and partial data structures. In this paper, we show how to integrate support for the magic wand into an automatic verier, requiring low specication overhead from the tool user. We present additional features to make the magic wand interact elegantly with abstract predicates, abstraction functions and \old" expressions. Our solution is compatible with a variety of logics and underlying implementation techniques. Our approach is implemented, and a prototype is available to download.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich, Department of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science