WP1: Floating-point analysis

This work package focuses on adapting static analysis and verification tools to deal accurately with floating-point computations. Using floating-point numbers to represent real numbers often yields to introduce subtle flaws in embedded C programs. In fact, many mathematical properties holding over the real numbers are compromised on floating-point numbers (for example, associativity of addition is lost). Consequently, the conformity of a computation with respect to the expected mathematical result is no longer guaranteed, which is unacceptable for C programs embedded in critical systems. In addition, although the IEEE 754 standard was introduced to specify how to implement basic floating-point operations, the result of a floating-point expression still depends on the features of the hardware computation unit. For example, the result of ternary expression a + b + c depends on the processor architecture in use, as IEEE 754 does not specify the format of intermediate computations (Intel performs intermediate computations on 80 bits while Sparc performs on 64 bits).

The primary goal of this work package is to implement an IEEE-754 conformant abstraction for floating point numbers that copes with all the basic operations (add, subs, mult, ...), all the formats (single, double and both extended), all the four rounding modes (to-the-nearest, to-zero, up, down) and to adapt our static analysis and verification tools to deal accurately with basic floating-point computations. We do not forecast to address in this project all the problems related to floating- point computations, but rather to focus on designing suitable abstractions for the IEEE standard and adapting the abstract domains of Frama-C on floating-point numbers.

Our secondary goal in this work package is to understand how floating-point computations are performed in industrial C code and to put at work our static analysis and verification tools on these programs. WP3 (Combining Static Analysis Techniques) in the sense that the floating-point specific analyses devised in WP1 will have to be combined with the other ones. In addition, as for all the other technical work packages, the availability of new analyzers will greatly help the dissemination of the Frama-C platform as envisaged in WP6 (Spreading Static Analysis).