FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
Abstract
Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.
Related
- Analysis and Detection of Stagnation in Floating-Point Summation
- Hyperspectral Anomaly Detection via Group Sparse Low-Rank Tensor Factorization With Automatic Anomaly Grouping
- Real-time and adaptive anomaly detection algorithm for cyclostationary models
- Moment-Based Anomaly Detection in High-Dimensional Mixed Data
- Statistical Feature Augmentation for Anomaly Detection in Dynamic Graphs
BibTeX
@misc{bortolussi2026fpscan,
title = {{FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection}},
author = {Julien Bortolussi and Dorra Ben Khalifa and Pierre-Loïc Garoche},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.07492},
eprint = {2609.07492},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.07492},
note = {CC BY-NC-SA 4.0},
}
RIS
TY - UNPB
TI - FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
AU - Julien Bortolussi
AU - Dorra Ben Khalifa
AU - Pierre-Loïc Garoche
PY - 2026
DA - 2026/09/07
PB - arXiv
DO - 10.48550/arxiv.2609.07492
UR - https://arxiv.org/abs/2609.07492
AB - Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.
ER -