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 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 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
|11:00 - 11:22|
BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-program Path Sampling and Per-path Abstract Interpretation
Zhuo ZhangPurdue University, Wei YouPurdue University, Guanhong TaoPurdue University, Guannan WeiPurdue University, Yonghwi KwonUniversity of Virginia, Xiangyu ZhangPurdue UniversityDOI Pre-print
|11:22 - 11:45|
|11:45 - 12:07|
Benno SteinUniversity of Colorado Boulder, Benjamin Barslev NielsenAarhus University, Bor-Yuh Evan ChangUniversity of Colorado Boulder | Amazon, Anders MøllerAarhus UniversityPre-print
|12:07 - 12:30|