
Open access
Date
2015Type
- Conference Paper
ETH Bibliography
yes
Altmetrics
Abstract
Permission-based verification logics such as separation logic have led to the development of many practical verification tools over the last decade. Verifiers 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 modifications 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 verification tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures. In this paper, we show how to integrate support for the magic wand into an automatic verifier, requiring low specification overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specification features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques. We have implemented our approach, and a prototype verifier is available to download, along with a collection of examples. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000104710Publication status
publishedExternal links
Editor
Book title
29th European Conference on Object-Oriented Programming (ECOOP 2015)Journal / series
Leibniz International Proceedings in Informatics (LIPIcs)Volume
Pages / Article No.
Publisher
Schloss Dagstuhl – Leibniz-Zentrum für InformatikEvent
Subject
Magic Wand; Software Verification; Automatic Verifiers; Separation Logic; Implicit Dynamic FramesOrganisational unit
03653 - Müller, Peter / Müller, Peter
More
Show all metadata
ETH Bibliography
yes
Altmetrics