Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations

TL;DR

This paper introduces two novel methods using Bernstein expansions and sparse Krivine-Stengle representations to compute rigorous upper bounds of roundoff errors in non-linear polynomial programs, enhancing validation of critical embedded software.

Contribution

The paper presents two new approaches adapted from global optimization to accurately bound roundoff errors, along with software implementations and performance comparisons.

Findings

Methods achieve competitive performance.

Accurate upper bounds are computed.

Software packages are released for practical use.

Abstract

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.