[ICFP24] Abstract Interpreters: a Monadic Approach to Modular Verification скачать в хорошем качестве

[ICFP24] Abstract Interpreters: a Monadic Approach to Modular Verification

Abstract Interpreters: A Monadic Approach to Modular Verification (Video, ICFP 2024) Sébastien Michelland, Yannick Zakowski, and Laure Gonnord (Université Grenoble-Alpes - Grenoble INP - LCIS, France; Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, France; Université Grenoble-Alpes - Grenoble INP - LCIS, France) 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. Article: https://doi.org/10.1145/3674646 Supplementary archive: https://doi.org/10.5281/zenodo.11470739 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) Supplementary web page: https://gitlab.inria.fr/sebmiche/itre... ORCID: https://orcid.org/0009-0000-5428-5433, https://orcid.org/0000-0003-4585-6470, https://orcid.org/0000-0002-8013-1611 Video Tags: Monadic Semantics, Abstract Interpretation, Formal Verification, icfp24main-p73-p, doi:10.1145/3674646, doi:10.5281/zenodo.11470739, orcid:0009-0000-5428-5433, orcid:0000-0003-4585-6470, orcid:0000-0002-8013-1611, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2024 conference, September 2–7, 2024, https://icfp24.sigplan.org/ Sponsored by ACM SIGPLAN,