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 AsGet 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
https://doi.org/10.4230/DARTS.9.2.8
Artifact
DARTS-9-2-8-artifact-8b2b29dad8ea433e43604d15e8358e58.tar
(Filesize: 1.39 GB)
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