The pitfalls of verifying floating-point computations

TL;DR

This paper discusses the challenges in verifying floating-point computations in critical systems, highlighting issues caused by semantics variations and proposing solutions for analysis tools.

Contribution

It provides concrete examples of floating-point verification problems and introduces solutions to improve analysis accuracy.

Findings

Semantic variations affect floating-point verification

Examples of verification problems in floating-point computations

Proposed solutions enhance analysis reliability

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.