License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2015.614
URN: urn:nbn:de:0030-drops-52408
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5240/
Go to the corresponding LIPIcs Volume Portal

Schwerhoff, Malte ; Summers, Alexander J.

Lightweight Support for Magic Wands in an Automatic Verifier

pdf-format:
30.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{schwerhoff_et_al:LIPIcs:2015:5240,
  author =	{Malte Schwerhoff and Alexander J. Summers},
  title =	{{Lightweight Support for Magic Wands in an Automatic Verifier}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{614--638},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{John Tang Boyland},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5240},
  URN =		{urn:nbn:de:0030-drops-52408},
  doi =		{10.4230/LIPIcs.ECOOP.2015.614},
  annote =	{Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames}
}

Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames
Collection: 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Issue Date: 2015
Date of publication: 29.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI