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.
Tue 25 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:00 - 14:30 | Proof Techniques and MechanizationResearch Papers at Stifel Theatre Chair(s): Niki Vazou University of Maryland, USA | ||
13:00 22mTalk | MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic Research Papers Robbert Krebbers Delft University of Technology, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Ralf Jung MPI-SWS, Joseph Tassarotti Carnegie Mellon University, Jan-Oliver Kaiser MPI-SWS, Amin Timany imec-Distrinet KU-Leuven, Arthur Charguéraud Inria, Derek Dreyer MPI-SWS DOI | ||
13:22 22mTalk | Mtac2: Typed Tactics for Backward Reasoning in Coq Research Papers Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET, Robbert Krebbers Delft University of Technology, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek Dreyer MPI-SWS DOI | ||
13:45 22mTalk | Compositional Soundness Proofs of Abstract Interpreters Research Papers Sven Keidel Delft University of Technology, Netherlands, Casper Bach Poulsen Delft University of Technology, Sebastian Erdweg Delft University of Technology, Netherlands DOI | ||
14:07 22mTalk | Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper Research Papers DOI |