FPScan finds critical errors in floating-point programs automatically
FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
Software Engineering
Summary
Floating-point programs, which use numbers with limited precision, are tricky to write correctly because tiny rounding mistakes can become large problems. FPScan is a new tool that helps find two types of serious errors where these small rounding issues get magnified. It works by analyzing the sizes of numbers in a program and setting up math constraints to check where errors could get very bad. The authors tested FPScan on standard benchmarks and compared it with other tools to show how well it detects these problems.
What this means in practice
- •For software developers: Detect critical floating-point errors early during development to improve numerical reliability of scientific and engineering applications.
- •For software testing teams: Automate identification of floating-point pitfalls like absorption and cancellation to enhance the effectiveness of testing procedures for numerical code.
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.