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 Times are displayed in time zone: Beirut change

 11:00 - 12:30: Abstract InterpretationOOPSLA at Attica Chair(s): John HughesChalmers University of Technology, Sweden 11:00 - 11:22Talk BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-Program Path Sampling and Per-Path Abstract InterpretationOOPSLAZhuo ZhangPurdue University, Wei YouPurdue University, Guanhong TaoPurdue University, Guannan WeiPurdue University, Yonghwi KwonUniversity of Virginia, Xiangyu ZhangPurdue University DOI Pre-print 11:22 - 11:45Talk Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programmingOOPSLAGuannan WeiPurdue University, Yuxuan ChenPurdue University, Tiark RompfPurdue University DOI 11:45 - 12:07Talk Static Analysis with Demand-Driven Value RefinementOOPSLABenno SteinUniversity of Colorado Boulder, Benjamin Barslev NielsenAarhus University, Bor-Yuh Evan ChangUniversity of Colorado Boulder | Amazon, Anders MøllerAarhus University DOI Pre-print 12:07 - 12:30Talk Sound and Reusable Components for Abstract InterpretationOOPSLASven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz DOI