License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.9.2.8
URN: urn:nbn:de:0030-drops-182485
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18248/
Go back to Dagstuhl Artifacts Series

Silver, Lucas ; Westbrook, Eddy ; Yacavone, Matthew ; Scott, Ryan

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

pdf-format:
DARTS-9-2-8.pdf (0.4 MB)

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.

BibTeX - Entry

@Article{silver_et_al:DARTS.9.2.8,
  author =	{Silver, Lucas and Westbrook, Eddy and Yacavone, Matthew and Scott, Ryan},
  title =	{{Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)}},
  pages =	{8:1--8:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Silver, Lucas and Westbrook, Eddy and Yacavone, Matthew and Scott, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18248},
  URN =		{urn:nbn:de:0030-drops-182485},
  doi =		{10.4230/DARTS.9.2.8},
  annote =	{Keywords: coinduction, specification, verification, monads}
}

Keywords: coinduction, specification, verification, monads
Collection: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Issue Date: 2023
Date of publication: 11.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI