Abstract Fixpoint Computations with Numerical Acceleration Methods

TL;DR

This paper introduces a novel approach to improve static program analysis by dynamically adapting the widening operator in fixpoint computations, leveraging numerical acceleration techniques to enhance precision and convergence.

Contribution

It presents a new method that integrates numerical analysis techniques into abstract interpretation to automatically and dynamically refine the widening operator.

Findings

Enhanced convergence speed of fixpoint computations

Improved precision in static analysis results

Automatic adaptation of widening operators

Abstract

Static analysis by abstract interpretation aims at automatically proving properties of computer programs. To do this, an over-approximation of program semantics, defined as the least fixpoint of a system of semantic equations, must be computed. To enforce the convergence of this computation, widening operator is used but it may lead to coarse results. We propose a new method to accelerate the computation of this fixpoint by using standard techniques of numerical analysis. Our goal is to automatically and dynamically adapt the widening operator in order to maintain precision.