DARTS.1.1.10.pdf
- Filesize: 355 kB
- 2 pages
Document
Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Volume: DARTS, Volume 1 (ECOOP 2015)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Germany license
- Publication Date: 2015-10-30
Artifact Description
Document Identifiers
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)
https://doi.org/10.4230/DARTS.1.1.10
https://doi.org/10.4230/DARTS.1.1.10
Artifact
darts-v001-i001-10-artifact-48b95a24e7cf17709871947c5d6b199b.zip
(Filesize: 348.7 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.
Keywords
- Magic Wand
- Software Verification
- Automatic Verifiers
- Separation Logic
- Implicit Dynamic Frames
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads