Tool detects hidden errors in computer calculations with floating points
FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
Software Engineering
Summary
Floating-point calculations in computer programs can sometimes produce big mistakes due to tiny rounding errors that get amplified, causing wrong results. The authors created FPScan, a tool that automatically finds two common and serious rounding error problems called absorption and catastrophic cancellation. FPScan works by analyzing the program’s variables to estimate their size and then uses logical reasoning to check if these errors might happen. They tested FPScan on a set of example programs and compared it to other tools to see how well it works and how fast it is.
floating-point arithmeticrounding errorcatastrophic cancellationabsorptionstatic analysisabstract interpretationconstraint solvingSMT solvernumerical precisionFPBench
Authors
Julien Bortolussi, Dorra Ben Khalifa, Pierre-Loïc Garoche
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.