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

Alexandre Rocca (1) , Victor Magron (1) , Thao Dang (1)

1 VERIMAG - IMAG - VERIMAG

Floating point error is an inevitable drawback of embedded systems implementation. Computing rigorous upper bounds of roundoff errors is absolutely necessary for the validation of critical software. This problem of computing rigorous upper bounds 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.

Mots clés: Polynomial Optimization; Floating Point Arithmetic; Roundoff Error Bounds; Linear Programming Relaxations; Bernstein Ex-; pansions; Krivine-Stengle Representations

Domaines: Optimisation et contrôle [math.OC]

Alexandre Rocca, Victor Magron, Thao Dang. Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations. 2017. ⟨hal-01448167⟩