Compositional soundness proofs of abstract interpreters

Sven Keidel, Casper Poulsen, Sebastian Erdweg

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

23 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
PublisherAssociation for Computing Machinery (ACM)
Number of pages26
Publication statusPublished - 1 Sep 2018


  • Abstract Interpretation
  • Static Analysis
  • Soundness


Dive into the research topics of 'Compositional soundness proofs of abstract interpreters'. Together they form a unique fingerprint.

Cite this