Abstract Interpreters: A Monadic Approach to Modular Verification
Article No.: 257, Pages 602 - 629
Abstract
We argue that monadic interpreters built as layers of interpretations stacked atop the free monad constitute a promising way to implement and verify abstract interpreters in dependently-typed theories such as the one underlying the Coq proof assistant. The approach enables modular proofs of soundness of the resulting interpreters. We provide generic abstract control flow combinators proven correct once and for all against their concrete counterpart. We demonstrate how to relate concrete handlers implementing effects to abstract variants of these handlers, essentially capturing the traditional soundness of transfer functions in the context of monadic interpreters. Finally, we provide generic results to lift soundness statements via the interpretation of stateful and failure effects. We formalize all the aforementioned combinators and theories in Coq, and demonstrate their benefits by implementing and proving correct two illustrative abstract interpreters for a structured imperative language and a toy assembly.
References
[1]
Martin Bodin, Philippa Gardner, Thomas P. Jensen, and Alan Schmitt. 2019. “ Skeletal semantics and their interpretations. ” Proc. ACM Program. Lang., 3, POPL, 44 : 1-44 : 31.
[2]
Sylvain Boulmé and Alexandre Maréchal. 2019. “ Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra.” J. Autom. Reason., 62, 4, 505-530.
[3]
Venanzio Capretta. July 2005. “ General Recursion via Coinductive Types.” Logical Methods in Computer Science, Volume 1, Issue 2, ( July 2005 ). 2 :1) 2005.
[4]
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. 2023. “Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. ” Proc. ACM Program. Lang., 7, POPL, 1770-1800. /3571254.
[5]
Agostino Cortesi, Giulia Costantini, and Pietro Ferrara. Sept. 2013. “A Survey on Product Operators in Abstract Interpretation.” Electronic Proceedings in Theoretical Computer Science, 129, (Sept. 2013 ).
[6]
Patrick Cousot. Sept. 2021. Principles of Abstract Interpretation. The MIT Press, (Sept. 2021 ). isbn: 9780262044905.
[7]
Patrick Cousot and Radhia Cousot. 1979. “ Systematic design of program analysis frameworks.” In: Principles of programming languages (POPL). ACM, 269-282.
[8]
David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn. Aug. 2017. “ Abstracting Definitional Interpreters (Functional Pearl). ” Proc. ACM Program. Lang., 1, ICFP, Article 12, (Aug. 2017 ), 25 pages.
[9]
David Darais, Matthew Might, and David Van Horn. 2015. “ Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis. ” In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2015 ). Association for Computing Machinery, Pittsburgh, PA, USA, 552-571. isbn: 9781450336895.
[10]
David Darais and David Van Horn. 2016. “ Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.” In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016 ). Association for Computing Machinery, Nara, Japan, 311-324. isbn: 9781450342193. 1934.
[11]
David Charles Darais. 2017. “ Mechanizing Abstract Interpretation.” Ph. D. Dissertation. University of Maryland, College Park, MD, USA.
[12]
Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno CdS Oliveira. 2013. “ Modular monadic meta-theory. ” ACM SIGPLAN Notices, 48, 9, 319-330.
[13]
Benjamin Delaware, Bruno C d. S. Oliveira, and Tom Schrijvers. 2013. “ Meta-theory à la carte.” In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 207-218.
[14]
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. “ CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.” In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16). USENIX Association, Savannah, GA, USA, 653-669. isbn: 9781931971331.
[15]
Peter Hancock and Anton Setzer. 2000. “Interactive Programs in Dependent Type Theory.” In: Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic. Springer-Verlag, Berlin, Heidelberg, 317-331. isbn: 3540678956.
[16]
John Hughes. May 2000. “ Generalising monads to arrows.” Science of Computer Programming, 37, (May 2000 ), 67-111. ( 99 ) 00023-4.
[17]
Ende Jin, Nada Amin, and Yizhou Zhang. 2023. “ Extensible metatheory mechanization via family polymorphism. ” Proceedings of the ACM on Programming Languages, 7, PLDI, 1608-1632.
[18]
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. “ A Formally-Verified C Static Analyzer.” In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. Ed. by Sriram K. Rajamani and David Walker. ACM, 247-259.
[19]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Dec. 2017. “ RustBelt: Securing the Foundations of the Rust Programming Language. ” Proc. ACM Program. Lang., 2, POPL, Article 66, (Dec. 2017 ), 34 pages.
[20]
Sven Keidel and Sebastian Erdweg. Oct. 2019. “Sound and reusable components for abstract interpretation. ” Proceedings of the ACM on Programming Languages, 3, (Oct. 2019 ), 1-28.
[21]
Sven Keidel, Sebastian Erdweg, and Tobias Hombücher. Aug. 2023. “ Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters. ” Proc. ACM Program. Lang., 7, ICFP, Article 221, (Aug. 2023 ), 27 pages.
[22]
Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg. July 2018. “Compositional Soundness Proofs of Abstract Interpreters. ” Proc. ACM Program. Lang., 2, ICFP, Article 72, ( July 2018 ), 26 pages.
[23]
Oleg Kiselyov and Hiromi Ishii. Aug. 2015. “Freer Monads, More Extensible Efects.” SIGPLAN Not., 50, 12, (Aug. 2015 ), 94-105.
[24]
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. “ From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server.” In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019 ). Association for Computing Machinery, Cascais, Portugal, 234-248. isbn: 9781450362221.
Index Terms
- Abstract Interpreters: A Monadic Approach to Modular Verification
Recommendations
Monadic abstract interpreters
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationRecent developments in the systematic construction of abstract interpreters hinted at the possibility of a broad unification of concepts in static analysis. We deliver that unification by showing context-sensitivity, polyvariance, flow-sensitivity, ...
Monadic abstract interpreters
PLDI '13Recent developments in the systematic construction of abstract interpreters hinted at the possibility of a broad unification of concepts in static analysis. We deliver that unification by showing context-sensitivity, polyvariance, flow-sensitivity, ...
Compositional soundness proofs of abstract interpreters
Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort. To reduce complexity and effort, we propose a ...
Comments
Information & Contributors
Information
Published In
August 2024
1031 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 August 2024
Published in PACMPL Volume 8, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 122Total Downloads
- Downloads (Last 12 months)122
- Downloads (Last 6 weeks)54
Reflects downloads up to 22 Oct 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in