The pitfalls of verifying floating-point computations
Programming Languages
2025-10-20 v5 Numerical Analysis
Numerical Analysis
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.
Cite
@article{arxiv.cs/0701192,
title = {The pitfalls of verifying floating-point computations},
author = {David Monniaux},
journal= {arXiv preprint arXiv:cs/0701192},
year = {2025}
}