Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 12:07 - 12:30 at Attica - Abstract Interpretation Chair(s): John Hughes

Abstract interpretation is a methodology for defining sound static analysis. Yet, building sound static analyses for modern programming languages is difficult, because these static analyses need to combine sophisticated abstractions for values, environments, stores, etc. However, static analyses often tightly couple these abstractions in the implementation, which not only complicates the implementation, but also makes it hard to decide which parts of the analyses can be proven sound independently from each other. Furthermore, this coupling makes it hard to combine soundness lemmas for parts of the analysis to a soundness proof of the complete analysis.

To solve this problem, we propose to construct static analyses modularly from \emph{reusable analysis components}. Each analysis component encapsulates a single analysis concern and can be proven sound independently from the analysis where it is used. We base the design of our analysis components on \emph{arrow transformers}, which allows us to compose analysis components. This composition preserves soundness, which guarantees that a static analysis is sound, if all its analysis components are sound. This means that analysis developers do not have to worry about soundness as long as they reuse sound analysis components. To evaluate our approach, we developed a library of 13 reusable analysis components in Haskell. We use these components to define a $k$-CFA analysis for PCF and an interval and reaching definition analysis for a While language.

Wed 23 Oct
Times are displayed in time zone: (GMT+03:00) Beirut change

11:00 - 12:30: OOPSLA - Abstract Interpretation at Attica
Chair(s): John HughesChalmers University of Technology, Sweden
splash-2019-oopsla11:00 - 11:22
Zhuo ZhangPurdue University, Wei YouPurdue University, Guanhong TaoPurdue University, Guannan WeiPurdue University, Yonghwi KwonUniversity of Virginia, Xiangyu ZhangPurdue University
DOI Pre-print
splash-2019-oopsla11:22 - 11:45
Guannan WeiPurdue University, Yuxuan ChenPurdue University, Tiark RompfPurdue University
splash-2019-oopsla11:45 - 12:07
Benno SteinUniversity of Colorado Boulder, Benjamin Barslev NielsenAarhus University, Bor-Yuh Evan ChangUniversity of Colorado Boulder | Amazon, Anders MøllerAarhus University
DOI Pre-print
splash-2019-oopsla12:07 - 12:30
Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz