Formal Proofs of Rounding Error Bounds
Pierre Roux
27 March 2015, 10h00 - 27 March 2015, 11h30 Salle/Bat : 435/PCRI-N
Contact :
Activités de recherche : Formalisation et preuves de programmes numériques
Résumé :
Floating-point arithmetic is a very efficient solution to
perform computations in the real field. However, it induces rounding
errors making results computed in floating-point differ from what
would be computed with reals. Although numerical analysis gives tools
to bound such differences, the proofs involved can be painful, hence
error prone. We thus investigate the ability of a proof assistant like
Coq to mechanically check such proofs. We demonstrate two different
results involving matrices, which are pervasive among numerical
algorithms, and show that a large part of the development effort can
be shared between them.
In this talk, a brief introduction to floating point roundings will
be given followed by an overview of the results.
