2026-07-23T15:38:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18248 2024-03-06T11:05:19Z ddc:004 open_access

Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact) Silver, Lucas Westbrook, Eddy Yacavone, Matthew Scott, Ryan coinduction specification verification monads 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lucas Silver and Eddy Westbrook and Matthew Yacavone and Ryan Scott 2023 Is Part Of DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.9.2.8 urn:nbn:de:0030-drops-182485 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.8 eng https://creativecommons.org/licenses/by/4.0/legalcode