| ||||
| ||||
![]() Title:FPScan: an Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection Conference:SYNASC 2026 Tags:Absorption, Catastrophic cancellation, Constraint generation, Floating-point arithmetic, SMT solver and Static analysis 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. FPScan: an Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection ![]() FPScan: an Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection | ||||
| Copyright © 2002 – 2026 EasyChair |
