Acceleration of the abstract fixpoint computation in numerical program analysis

AbstractStatic analysis by abstract interpretation aims at automatically proving properties of computer programs, by computing invariants that over-approximate the program behaviors. These invariants are defined as the least fixpoint of a system of semantic equations and are most often computed using the Kleene iteration. This computation may not terminate so specific solutions were proposed to deal with this issue. Most of the proposed methods sacrifice the precision of the solution to guarantee the termination of the computation in a finite number of iterations. In this article, we define a new method which allows to obtain a precise fixpoint in a short time. The main idea is to use numerical methods designed for accelerating the convergence of numerical sequences. These methods were primarily designed to transform a convergent, real valued sequence into another sequence that converges faster to the same limit. In this article, we show how they can be integrated into the Kleene iteration in order to improve the fixpoint computation in the abstract interpretation framework. An interesting feature of our method is that it remains very close to the Kleene iteration and thus can be easily implemented in existing static analyzers. We describe a general framework and its application to two numerical abstract domains: the interval domain and the octagon domain. Experimental results show that the number of iterations and the time needed to compute the fixpoint undergo a significant reduction compared to the Kleene iteration, while its precision is preserved