⚠️ WARNING: FPANVerifier's SELTZO lemma system is currently being redesigned to improve verification performance, causing some temporary regressions in the strength of the results that FPANVerifier can prove. Please wait until the redesign is complete to obtain precise error bounds and non-overlapping guarantees.
FPANVerifier is an automatic theorem prover that verifies the correctness of floating-point algorithms. It uses a novel reasoning technique called the SELTZO abstraction to precisely track the propagation of rounding errors through multiple interdependent operations.
FPANVerifier handles a specific class of algorithms called floating-point accumulation networks (FPANs), which are branch-free sequences of floating-point sum and TwoSum operations. These algorithms are used to implement fast high-precision arithmetic and form the backbone of high-performance libraries like MultiFloats.jl, QD, XBLAS, and CAMPARY.
Despite being widely used, FPANs are notoriously difficult to analyze, and even expert numerical analysts have made mistakes leading to the publication of incorrect algorithms and false error bounds. FPANVerifier turns the tedious, error-prone process of manual rounding error analysis into a fully automated computation with rigorous formal correctness guarantees.
FPANVerifier is several million times faster than standard floating-point verification tools, including Z3, CVC5, MathSAT, and Bitwuzla. It solves problems in seconds that other tools need hours to days to answer, if at all. The bit-precise reasoning capability of the SELTZO abstraction allows FPANVerifier to solve problems that are impossible for interval-based tools like COLIBRI and dReal.
| Z3 | CVC5 | MathSAT | Bitwuzla | Colibri2 | dReal | FPANVerifier | |
|---|---|---|---|---|---|---|---|
| Float16 | > 3 days | 2.0 hours | 2.7 days | 1.2 hours | N/A | N/A | 0.7 sec |
| BFloat16 | > 3 days | 15.8 hours | > 3 days | 1.7 hours | N/A | N/A | 0.7 sec |
| Float32 | > 3 days | 17.0 hours | > 3 days | 8.6 hours | N/A | N/A | 0.7 sec |
| Float64 | > 3 days | > 3 days | > 3 days | > 3 days | N/A | N/A | 0.9 sec |
| Float128 | > 3 days | > 3 days | > 3 days | > 3 days | N/A | N/A | 1.0 sec |