Write a Blog >>
SPLASH 2019
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

Displayed time zone: Beirut change

11:00 - 12:30
Abstract InterpretationOOPSLA at Attica
Chair(s): John Hughes Chalmers University of Technology, Sweden
11:00
22m
Talk
BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-Program Path Sampling and Per-Path Abstract InterpretationACM SIGPLAN Distinguished Paper Award
OOPSLA
Zhuo Zhang Purdue University, Wei You Purdue University, Guanhong Tao Purdue University, Guannan Wei Purdue University, Yonghwi Kwon University of Virginia, Xiangyu Zhang Purdue University
DOI Pre-print
11:22
22m
Talk
Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programming
OOPSLA
Guannan Wei Purdue University, Yuxuan Chen Purdue University, Tiark Rompf Purdue University
DOI
11:45
22m
Talk
Static Analysis with Demand-Driven Value Refinement
OOPSLA
Benno Stein University of Colorado Boulder, Benjamin Barslev Nielsen Aarhus University, Bor-Yuh Evan Chang University of Colorado Boulder | Amazon, Anders Møller Aarhus University
DOI Pre-print
12:07
22m
Talk
Sound and Reusable Components for Abstract Interpretation
OOPSLA
Sven Keidel JGU Mainz, Sebastian Erdweg JGU Mainz
DOI