Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification
No abstract available.
Related papers
- Interaction trees: representing recursive and impure programs in Coq POPL 2020
- Dijkstra monads forever: termination-sensitive specifications for interaction trees POPL 2021
- TreeFuser: a framework for analyzing and fusing general recursive tree traversals OOPSLA 2017
- From C to interaction trees: specifying, verifying, and testing a networked server CPP 2019
- Context-Dependent Effects in Guarded Interaction Trees ESOP 2025
- On fusing recursive traversals of K-d trees CC 2016
- Schedgehammer: Auto-tuning Compiler Optimizations beyond Numerical Parameters CC 2026
- The WhyRel Prototype for Modular Relational Verification of Pointer Programs TACAS 2023