Decoupling the ascending and descending phases in Abstract Interpretation

TL;DR

This paper introduces a novel approach to abstract interpretation by decoupling the ascending and descending phases, replacing the abstract domain before the descending phase to improve precision, supported by theoretical justification and preliminary experiments.

Contribution

It proposes a simple variation of classical abstract interpretation that replaces the domain before the descending phase to enhance analysis precision.

Findings

Significant precision improvements observed in preliminary experiments.

The approach is justified within the A$^2$I framework.

Effective across various domain choices.

Abstract

Abstract Interpretation approximates the semantics of a program by mimicking its concrete fixpoint computation on an abstract domain $\mathbb{A}$. The abstract (post-) fixpoint computation is classically divided into two phases: the ascending phase, using widenings as extrapolation operators to enforce termination, is followed by a descending phase, using narrowings as interpolation operators, so as to mitigate the effect of the precision losses introduced by widenings. In this paper we propose a simple variation of this classical approach where, to more effectively recover precision, we decouple the two phases: in particular, before starting the descending phase, we replace the domain $\mathbb{A}$ with a more precise abstract domain $\mathbb{D}$. The correctness of the approach is justified by casting it as an instance of the A$^2$I framework. After demonstrating the new technique on a simple example, we summarize the results of a preliminary experimental evaluation, showing that it is able to obtain significant precision improvements for several choices of the domains $\mathbb{A}$ and $\mathbb{D}$.