Numerical programs: from roundoff-error detection to accurate formula synthesis

Опубликовано 28 июля 2016, 0:05

Exact computations being in general not track able for computers, they are approximated by floating-point computations. This is the source of many errors in numerical programs. Because the floating-point arithmetic is not intuitive, these errors are very difficult to detect and to correct. In this talk, we will focus on the detection of significant roundoff errors in existing codes and on the synthesis of new accurate formulas. We consider that a program would return an exact result if the computations were carried out using real numbers. In practice, roundoff errors arise during the execution and these errors are closely related to the way formulas are written. We start by presenting static analysis techniques to globally validate the accuracy of a numerical code and to detect the main sources of inaccuracy. This information provides some hints to the programmers, in order to enhance by hand their programs. Next, we present recent work on how to synthetize new expressions, mathematically equivalent to the original ones and more accurate. Our approach is based on abstract interpretation. We introduce Abstract Program Equivalence Graphs (APEGs) to represent in polynomial size an exponential number of mathematically equivalent expressions. The concretization of an APEG yields expressions of very different shapes and accuracies. Then, we extract optimized expressions from APEGs by searching the most accurate concrete expressions among the set of represented expressions.