The pitfalls of verifying floating-point computations

TL;DR

This paper investigates how floating-point semantics diverge across hardware, compilers, and libraries, jeopardising both testing and formal verification of critical systems. It catalogs concrete pitfalls, from IEEE-754 rounding and double rounding to architecture-specific behaviours on x87/SSE and PowerPC, and discusses their implications for program analysis, Hoare logic, and abstract interpretation. The authors propose pragmatic remedies (e.g., -ffloat-store, SSE usage, long double computations, assembly-level semantics, nondeterministic Hoare rules, and robust abstract domains) and illustrate them with realistic examples, including a modulo-like function and real-world code. The work emphasizes that reproducibility and sound modeling are essential for safety-critical FP software, and it advocates cautious use of optimisations and rigorous semantic foundations for verification tools.

Abstract

Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.