License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.30
URN: urn:nbn:de:0030-drops-182239
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18223/
Silver, Lucas ;
Westbrook, Eddy ;
Yacavone, Matthew ;
Scott, Ryan
Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification
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
@InProceedings{silver_et_al:LIPIcs.ECOOP.2023.30,
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}},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
pages = {30:1--30:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-281-5},
ISSN = {1868-8969},
year = {2023},
volume = {263},
editor = {Ali, Karim and Salvaneschi, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18223},
URN = {urn:nbn:de:0030-drops-182239},
doi = {10.4230/LIPIcs.ECOOP.2023.30},
annote = {Keywords: coinduction, specification, verification, monads}
}
