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

Authors Malte Schwerhoff, Alexander J. Summers

Thumbnail PDF

Artifact Description

  • Filesize: 355 kB
  • 2 pages

Document Identifiers

Author Details

Malte Schwerhoff
Alexander J. Summers

Cite AsGet BibTex

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)



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.
  • Magic Wand
  • Software Verification
  • Automatic Verifiers
  • Separation Logic
  • Implicit Dynamic Frames


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail