Static Analysis of Numerical Algorithms
Eric Goubault (CEA Saclay) and Sylvie Putot (CEA Saclay)
Abstract
We present a new numerical abstract domain for static analysis of the errors introduced by the approximation by floating-point arithmetic of real numbers computation, by abstract interpretation. This work extends a former domain (Goubault, SAS'01; Martel, ESOP'02), with a weakly relational domain for the approximation of the floating-point values of variables, based on affine arithmetic as first introduced for static analysis in (Putot and Goubault, NSAD'05). It allows us to analyze non trivial numerical computations, that no other abstract domain we know of can analyze with such precise results, such as linear recursive filters of different orders, Newton methods for solving non-linear equations, polynomial iterations, conjugate gradient algorithms etc.