Document Open Access Logo

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

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.30.pdf
  • Filesize: 0.84 MB
  • 26 pages

Document Identifiers

Author Details

Lucas Silver
  • University of Pennsylvania, Philadelphia, PA, USA
Eddy Westbrook
  • Galois, Inc., Portland, OR, USA
Matthew Yacavone
  • Galois, Inc., Portland, OR, USA
Ryan Scott
  • Galois, Inc., Portland, OR, USA

Cite AsGet BibTex

Lucas Silver, Eddy Westbrook, Matthew Yacavone, and Ryan Scott. Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.30

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Programming logic
  • Theory of computation → Separation logic
Keywords
  • coinduction
  • specification
  • verification
  • monads

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martinez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra monads for free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017. Google Scholar
  2. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge University Press, USA, 2014. Google Scholar
  3. Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. Leveraging rust types for modular specification and verification. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2019. Google Scholar
  4. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1999. Google Scholar
  5. Aaron R. Bradley. Sat-based model checking without unrolling. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011. Google Scholar
  6. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 418-430, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/2034773.2034828.
  7. Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. Continuous formal verification of amazon s2n. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), 2018. Google Scholar
  8. Jeremy Gibbons and Ralf Hinze. Just do it: simple monadic equational reasoning. In Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (ICFP), 2011. Google Scholar
  9. Paul He, Edwin Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic. A type system for extracting functional specifications from memory-safe imperative programs. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2021. Google Scholar
  10. Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547647.
  11. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  12. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 256-269. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951943.
  13. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP '09, pages 207-220, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1629575.1629596.
  14. Xavier Leroy and Sandrine Blazy. Formal verification of a c-like memory model and its uses for verifying program transformations. J. Autom. Reason., 41(1):1-31, July 2008. URL: https://doi.org/10.1007/s10817-008-9099-0.
  15. Giuliano Losa and Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), 2020. Google Scholar
  16. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, and Éric Tanter. Dijkstra monads for all. Proc. ACM Program. Lang., 3(ICFP), July 2019. URL: https://doi.org/10.1145/3341708.
  17. Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. Rusthornbelt: A semantic foundation for functional verification of rust programs with unsafe code. In Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2022. Google Scholar
  18. Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. Rusthorn: Chc-based verification for rust programs. In Proceedings of the 29th European Symposium on Programming (ESOP), 2020. Google Scholar
  19. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS), 1989. Google Scholar
  20. Eugenio Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1), 1989. Google Scholar
  21. Andrew M. Pitts. Evaluation logic. In Proceedings of the IV Higher Order Workshop, 1990. Google Scholar
  22. Gordon Plotkin and Matija Pretnar. A logic for algebraic effects. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS), 2008. Google Scholar
  23. Christoph Rauch, Sergey Goncharov, and Lutz Schröder. Generic hoare logic for order-enriched effects with exceptions. In Phillip James and Markus Roggenbach, editors, Recent Trends in Algebraic Development Techniques, pages 208-222, Cham, 2017. Springer International Publishing. Google Scholar
  24. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, pages 77-87, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2737924.2737964.
  25. Lucas Silver and Steve Zdancewic. Dijkstra monads forever: Termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434307.
  26. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 266-278, 2011. URL: https://doi.org/10.1145/2034773.2034811.
  27. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in f*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 256-270, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2837614.2837655.
  28. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. Verifying higher-order programs with the dijkstra monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 387-398, 2013. URL: https://doi.org/10.1145/2491956.2491978.
  29. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371119.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact