Verification of the functional behavior of a floating-point program: An industrial case study

• We analyze a critical C code involving floating-point computations.
• The code is dealing with rotations represented by quaternions.
• A functional requirement is given, about the norms of quaternions involved.
• We express the requirement in a formal specification language.
• Code is verified with respect to the specification using theorem proving.

We report a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving.