DROPS

Document

Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)

Authors: Malte Schwerhoff and Alexander J. Summers

Published in: DARTS, Volume 1, Issue 1, Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract

This artifact is based on Silicon, which is an automatic verification tool for programs written in the Silver Intermediate Verification Language. Silver is designed to natively support permission-based reasoning, in the style of separation logic and similar approaches. Our extension of Silicon provides support for specification and verification of programs using the magic wand operator, which can be used to represent ways to exchange views on the program state, or to represent partial versions of data structures. Our implementation is a backwards-compatible extension of the basic tool, and is provided along with a test suite of examples and regressions in a VirtualBox image. Instructions for running our tool on these (and user-defined) examples are provided in the image, to allow users to experiment with the verifier.

Cite as

Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{schwerhoff_et_al:DARTS.1.1.10,
  author =	{Schwerhoff, Malte and Summers, Alexander J.},
  title =	{{Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Schwerhoff, Malte and Summers, Alexander J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.10},
  URN =		{urn:nbn:de:0030-drops-55192},
  doi =		{10.4230/DARTS.1.1.10},
  annote =	{Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2015.614

Lightweight Support for Magic Wands in an Automatic Verifier

Authors: Malte Schwerhoff and Alexander J. Summers

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

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.

Cite as

Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 614-638, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schwerhoff_et_al:LIPIcs.ECOOP.2015.614,
  author =	{Schwerhoff, Malte and Summers, Alexander J.},
  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 =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.614},
  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}
}

Search Results

Documents authored by Schwerhoff, Malte

Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)

Abstract

Cite as

Lightweight Support for Magic Wands in an Automatic Verifier

Abstract

Cite as

Thanks for your feedback!

Could not send message