Compositional soundness proofs of abstract interpreters
- Publikationstyp:
- Zeitschriftenaufsatz
- Metadaten:
-
- Abstract
- <jats:p> Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high <jats:italic>proof complexity</jats:italic> and <jats:italic>proof effort</jats:italic> . To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem. </jats:p> <jats:p> To further reduce proof effort, we explore the relationship between soundness and parametricity. Parametricity not only provides us with useful guidelines for how to design non-leaky interfaces for shared interpreters, but also provides us soundness of shared pure functions as <jats:italic>free theorems</jats:italic> . We implemented our framework in Haskell and developed a <jats:italic>k</jats:italic> -CFA analysis for PCF and a tree-shape analysis for Stratego. We were able to prove both analyses sound compositionally with manageable complexity and effort, compared to a conventional soundness proof. </jats:p>
- Autoren
- Sven Keidel
- Casper Bach Poulsen
- Sebastian Erdweg
- DOI
- 10.1145/3236767
- eISSN
- 2475-1421
- Ausgabe der Veröffentlichung
- ICFP
- Zeitschrift
- Proceedings of the ACM on Programming Languages
- Sprache
- en
- Online publication date
- 2018
- Paginierung
- 1 - 26
- Datum der Veröffentlichung
- 2018
- Status
- Published
- Herausgeber
- Association for Computing Machinery (ACM)
- Herausgeber URL
- http://dx.doi.org/10.1145/3236767
- Datum der Datenerfassung
- 2022
- Titel
- Compositional soundness proofs of abstract interpreters
- Ausgabe der Zeitschrift
- 2
Datenquelle: Crossref
- Andere Metadatenquellen:
-
- Autoren
- Sven Keidel
- Casper Bach Poulsen
- Sebastian Erdweg
- Zeitschrift
- Proc. ACM Program. Lang.
- Artikelnummer
- ICFP
- Paginierung
- 72:1 - 72:1
- Datum der Veröffentlichung
- 2018
- Titel
- Compositional soundness proofs of abstract interpreters.
- Ausgabe der Zeitschrift
- 2
Datenquelle: DBLP
- Beziehungen:
- Eigentum von