Français Anglais
Accueil Annuaire Plan du site
Accueil > Evenements > Séminaires
Séminaire d'équipe(s) VALS
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.

Pour en savoir plus :
Séminaires
Programming computing media
Combinatoire
Friday 20 March 2020 - 14h30
Salle : 445 - PCRI-N
Frédéric Gruau .............................................

Forum dev-LRI
Wednesday 05 February 2020 - 14h00
Salle : 455 - PCRI-N
Erik Bray .............................................

Quantum at LRI
Calcul quantique
Tuesday 04 February 2020 - 09h00
Salle : 465 - PCRI-N
.............................................

Progressive Data Analysis: a new computation parad
Gestion de données du Web
Friday 24 January 2020 - 14h00
Salle : 435 - PCRI-N
Jean-Daniel Fekete .............................................

Jeux d’instructions : des extensions SIMD aux exte
Architectures parallèles
Tuesday 21 January 2020 - 10h30
Salle : 465 - PCRI-N
Daniel Etiemble .............................................