Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification

Autor:	Silver, Lucas, Westbrook, Eddy, Yacavone, Matthew, Scott, Ryan
Jazyk:	angličtina
Rok vydání:	2023
Předmět:	specification Theory of computation → Programming logic Theory of computation → Separation logic monads verification Theory of computation → Denotational semantics coinduction
DOI:	10.4230/lipics.ecoop.2023.30
Popis:	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. LIPIcs, Vol. 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 30:1-30:26
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::990f888391d1f1d4000b50e1183704a8 Zobrazit plný text záznamu