License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.1.1.10
URN: urn:nbn:de:0030-drops-55192
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5519/
Go back to Dagstuhl Artifacts Series

Schwerhoff, Malte ; Summers, Alexander J.

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

pdf-format:
10.pdf (0.3 MB)

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.

BibTeX - Entry

@Article{schwerhoff_et_al:DARTS:2015:5519,
  author =	{Malte Schwerhoff and Alexander J. Summers},
  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},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5519},
  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}
}

Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames
Collection: DARTS, Volume 1, Issue 1
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.614
Issue Date: 2015
Date of publication: 30.10.2015

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