Accelerated Data-Flow Analysis

TL;DR

This paper extends acceleration techniques from symbolic verification to data-flow analysis, providing a precise, efficient cubic-time algorithm for solving interval constraints with multiplication, enhancing the speed of fix-point computations.

Contribution

It introduces a novel acceleration framework for data-flow analysis that maintains precision and efficiency, including a cubic-time algorithm for interval constraints with multiplication.

Findings

Effective acceleration framework for data-flow analysis.

Cubic-time algorithm for solving interval constraints with multiplication.

Maintains precision without sacrificing efficiency.

Abstract

Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.