Accurate Evaluation of Arithmetic Expressions (Invited Talk)

In this article, we focus on the synthesis of arithmetic expressions that can be evaluated efficiently on computers in the sense that they do not create overflows, are accurate and do not use unnecessary ressources. We consider several computer arithmetics for integers, floating-point and fixed-point numbers and intervals and we show how to synthetize new expressions, mathematically equivalent to the original ones and more efficient. Our approach is based on abstract interpretation. We introduce two abstractions to represent in polynomial size sets of mathematically equivalent expressions. Then, we extract optimized expressions by searching the most accurate expression among the expressions contained in the abstract structures. We focus on the correctness of the synthesis which consists of showing that the new expressions cannot be distinguished from the source expressions when an observational abstraction is used.