Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
- Publication type:
- Journal article
- Metadata:
-
- Autoren
- Sven Keidel
- Sebastian Erdweg
- Tobias Hombuecher
- Autoren-URL
- https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=fis-test-1&SrcAuth=WosAPI&KeyUT=WOS:001063711900034&DestLinkType=FullRecord&DestApp=WOS_CPL
- DOI
- 10.1145/3607863
- eISSN
- 2475-1421
- Externe Identifier
- Clarivate Analytics Document Solution ID: R3XL3
- Ausgabe der Veröffentlichung
- ICFP
- Zeitschrift
- PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
- Schlüsselwörter
- Big-Step Abstract Interpretation
- Static Analysis
- Fixpoint Algorithm
- Artikelnummer
- ARTN 221
- Datum der Veröffentlichung
- 2023
- Status
- Published
- Titel
- Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
- Sub types
- Article
- Ausgabe der Zeitschrift
- 7
Data source: Web of Science (Lite)
- Other metadata sources:
-
- Abstract
- <jats:p>Big-step abstract interpreters are an approach to build static analyzers based on big-step interpretation. While big-step interpretation provides a number of benefits for the definition of an analysis, it also requires particularly complicated fixpoint algorithms because the analysis definition is a recursive function whose termination is uncertain. This is in contrast to other analysis approaches, such as small-step reduction, abstract machines, or graph reachability, where the analysis essentially forms a finite transition system between widened analysis states.</jats:p> <jats:p>We show how to systematically develop sophisticated fixpoint algorithms for big-step abstract interpreters and how to ensure their soundness. Our approach is based on small and reusable fixpoint combinators that can be composed to yield fixpoint algorithms. For example, these combinators describe the order in which the program is analyzed, how deep recursive functions are unfolded and loops unrolled, or they record auxiliary data such as a (context-sensitive) call graph. Importantly, each combinator can be developed separately, reused across analyses, and can be verified sound independently. Consequently, analysis developers can freely compose combinators to obtain sound fixpoint algorithms that work best for their use case. We provide a formal metatheory that guarantees a fixpoint algorithm is sound if its composed from sound combinators only. We experimentally validate our combinator-based approach by describing sophisticated fixpoint algorithms for analyses of Stratego, Scheme, and WebAssembly.</jats:p>
- Autoren
- Sven Keidel
- Sebastian Erdweg
- Tobias Hombücher
- DOI
- 10.1145/3607863
- eISSN
- 2475-1421
- Ausgabe der Veröffentlichung
- ICFP
- Zeitschrift
- Proceedings of the ACM on Programming Languages
- Sprache
- en
- Online publication date
- 2023
- Paginierung
- 955 - 981
- Datum der Veröffentlichung
- 2023
- Status
- Published
- Herausgeber
- Association for Computing Machinery (ACM)
- Herausgeber URL
- http://dx.doi.org/10.1145/3607863
- Datum der Datenerfassung
- 2024
- Titel
- Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
- Ausgabe der Zeitschrift
- 7
Data source: Crossref
- Autoren
- Sven Keidel
- Sebastian Erdweg
- Tobias Hombücher
- Zeitschrift
- Proc. ACM Program. Lang.
- Artikelnummer
- ICFP
- Paginierung
- 955 - 981
- Datum der Veröffentlichung
- 2023
- Titel
- Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters.
- Ausgabe der Zeitschrift
- 7
Data source: DBLP
- Beziehungen:
- Property of