Standard

Compositional soundness proofs of abstract interpreters. / Keidel, Sven; Poulsen, Casper; Erdweg, Sebastian.

Proceedings of the ACM on Programming Languages. Vol. 2 ICFP. ed. Association for Computing Machinery (ACM), 2018. 72.

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

Harvard

Keidel, S, Poulsen, C & Erdweg, S 2018, Compositional soundness proofs of abstract interpreters. in Proceedings of the ACM on Programming Languages. ICFP edn, vol. 2, 72, Association for Computing Machinery (ACM). https://doi.org/10.1145/3236767

APA

Keidel, S., Poulsen, C., & Erdweg, S. (2018). Compositional soundness proofs of abstract interpreters. In Proceedings of the ACM on Programming Languages (ICFP ed., Vol. 2). [72] Association for Computing Machinery (ACM). https://doi.org/10.1145/3236767

Vancouver

Keidel S, Poulsen C, Erdweg S. Compositional soundness proofs of abstract interpreters. In Proceedings of the ACM on Programming Languages. ICFP ed. Vol. 2. Association for Computing Machinery (ACM). 2018. 72 https://doi.org/10.1145/3236767

Author

Keidel, Sven ; Poulsen, Casper ; Erdweg, Sebastian. / Compositional soundness proofs of abstract interpreters. Proceedings of the ACM on Programming Languages. Vol. 2 ICFP. ed. Association for Computing Machinery (ACM), 2018.

BibTeX

@inproceedings{605f2cb0a8c54086aa2985f38f4db1ed,
title = "Compositional soundness proofs of abstract interpreters",
abstract = "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 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. 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 free theorems. We implemented our framework in Haskell and developed a k-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.",
keywords = "Abstract Interpretation, Static Analysis, Soundness",
author = "Sven Keidel and Casper Poulsen and Sebastian Erdweg",
year = "2018",
month = "9",
day = "1",
doi = "10.1145/3236767",
language = "English",
volume = "2",
booktitle = "Proceedings of the ACM on Programming Languages",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",
edition = "ICFP",

}

RIS

TY - GEN

T1 - Compositional soundness proofs of abstract interpreters

AU - Keidel, Sven

AU - Poulsen, Casper

AU - Erdweg, Sebastian

PY - 2018/9/1

Y1 - 2018/9/1

N2 - 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 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. 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 free theorems. We implemented our framework in Haskell and developed a k-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.

AB - 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 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. 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 free theorems. We implemented our framework in Haskell and developed a k-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.

KW - Abstract Interpretation

KW - Static Analysis

KW - Soundness

U2 - 10.1145/3236767

DO - 10.1145/3236767

M3 - Conference contribution

VL - 2

BT - Proceedings of the ACM on Programming Languages

PB - Association for Computing Machinery (ACM)

ER -

ID: 47448709