For example, reasoning about dynamic property accesses sometimes requires precise relational information connecting the object, the dynamically-computed property name, and the property value.
Even a minor precision loss at such critical program locations can result in a proliferation of spurious dataflow that renders the analysis results useless.
We present a technique by which a conventional non-relational static dataflow analysis can be combined soundly with a value refinement mechanism to increase precision on demand at critical locations.
Crucially, our technique is able to incorporate relational information from the value refinement mechanism into the non-relational domain of the dataflow analysis.
Wed 23 OctDisplayed time zone: Beirut change
11:00 - 12:30
|BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-Program Path Sampling and Per-Path Abstract Interpretation|
Zhuo Zhang Purdue University, Wei You Purdue University, Guanhong Tao Purdue University, Guannan Wei Purdue University, Yonghwi Kwon University of Virginia, Xiangyu Zhang Purdue UniversityDOI Pre-print
|Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programming|
|Static Analysis with Demand-Driven Value Refinement|
Benno Stein University of Colorado Boulder, Benjamin Barslev Nielsen Aarhus University, Bor-Yuh Evan Chang University of Colorado Boulder | Amazon, Anders Møller Aarhus UniversityDOI Pre-print
|Sound and Reusable Components for Abstract Interpretation|