Semantics-Based Transformation of Arithmetic Expressions

Floating-point arithmetic is an important source of errors in programs because of the loss of precision arising during a computation. Unfortunately, this arithmetic is not intuitive (e.g. many elementary operations are not associative, inversible, etc.) making the debugging phase very difficult and empiric. This article introduces a new kind of program transformation in order to automatically improve the accuracy of floating-point computations. We use P. Cousot and R. Cousot’s framework for semantics program transformation and we propose an offline transformation. This technique was implemented, and the first experimental results are presented.

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: Matthieu Martel
• Keywords: Floating-Point Arithmetic, Formal Methods, Program Transformation, SAS 2007, Semantics Program Transformation