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

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.

Speaker Bios

Matthieu Martel is Associate Professor at the University of Perpignan (France) and head of the DALI research team at the Montpellier Laboratory of Informatics, Robotics, and Microelectronics (LIRMM in French), a cross-faculty research entity of the University of Montpellier 2 (UM2) and the National Center for Scientific Research (CNRS). Matthieu Martel has been working for ten years on static analysis techniques to assert the numerical accuracy of floating-point computations. Applications of his work concern the validation of critical embedded software, mainly for the aeraunotic industry. From 2000 to 2007 Matthieu Martel was associate professor at Ecole Polytechnique, in Paris and researcher at Commissariat at Energie Atomique (the french institute for atomic energy) where he contributed to develop the Fluctuat tool, a static analyzer used by aeronautic companies to validate the accuracy of floating-pointcomputations in embedded codes. Since 2007, Matthieu Martel develops, at the University of Perpignan, the SARDANA project on the synthesis of numerically accurate codes using floating-point computations. In 2010, Matthieu Martelwas the general co-chair (with Radhia Cousot) of the 17th International Static Analysis Symposium, one of the main conferences in static analysis.