Abstract interpretation is a general framework for expressing static program analyses. It reduces the problem of extracting properties of a program to computing an approximation of the least fixpoint of a system of equations. The de facto approach for computing this approximation uses a Bourdoncle’s algorithm based on weak topological order (WTO). This talk describes recent work on improving the time and memory performance of abstract interpretation without sacrificing precision. First, we present a deterministic parallel algorithm for fixpoint computation by introducing the notion of weak partial order (WPO), which generalizes the notion of WTO. We present an almost-linear time algorithm for computing a WPO. Second, we present a technique for memory-efficient fixpoint computation. Both techniques are proved to be optimal while computing the same result as Bourdoncle’s approach. The talk will also describe the implementation and evaluation of these techniques in the NASA IKOS and Facebook SPARTA abstract interpreters.
Presented at the
Workshop on Research Highlights in Programming Languages at FSTTCS 2020.
- Tags
-
