DARTS.9.2.8.pdf
- Filesize: 399 kB
- 2 pages
Document
Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
Artifact Description
Document Identifiers
Cite As Get BibTex
Lucas Silver, Eddy Westbrook, Matthew Yacavone, and Ryan Scott. Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DARTS.9.2.8
Artifact
DARTS-9-2-8-artifact-8b2b29dad8ea433e43604d15e8358e58.tar
(Filesize: 1.39 GB)
MD5 Sum:
8b2b29dad8ea433e43604d15e8358e58
(Get MD5 Sum)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy
Abstract
This paper presents a specification framework for monadic, recursive, interactive programs that supports auto-active verification, an approach that combines user-provided guidance with automatic verification techniques. This verification tool is designed to have the flexibility of a manual approach to verification along with the usability benefits of automatic approaches. We accomplish this by augmenting Interaction Trees, a Coq datastructure for representing effectful computations, with logical quantifier events. We show that this yields a language of specifications that are easy to understand, automatable, and are powerful enough to handle properties that involve non-termination. Our framework is implemented as a library in Coq. We demonstrate the effectiveness of this framework by verifying real, low-level code.
Subject Classification
ACM Subject Classification
- Theory of computation → Denotational semantics
- Theory of computation → Programming logic
- Theory of computation → Separation logic
Keywords
- coinduction
- specification
- verification
- monads
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads