Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
For developers of critical embedded software, this work provides new techniques to certify floating-point error bounds in non-linear programs.
The paper introduces two new methods based on Bernstein expansions and sparse Krivine-Stengle representations to compute rigorous upper bounds of roundoff errors for polynomial programs, releasing tools FPBern and FPKiSten that achieve competitive accuracy compared to state-of-the-art tools.
Floating point error is an inevitable drawback of embedded systems implementation. Computing rigorous upper bounds of roundoff errors is absolutely necessary to the validation of critical software. This problem is even more challenging when addressing non-linear programs. In this paper, we propose and compare two new methods based on Bernstein expansions and sparse Krivine-Stengle representations, adapted from the field of the global optimization to compute upper bounds of roundoff errors for programs implementing polynomial functions. We release two related software package FPBern and FPKiSten, and compare them with state of the art tools. We show that these two methods achieve competitive performance, while computing accurate upper bounds by comparison with other tools.