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
Knowledge Graph Refinement based on Triplet BERT-N
Gestion de données du Web
Monday 29 November 2021 - 13h00
Salle : 455 - PCRI-N
Armita Khajeh Nassiri .............................................

A Hyper-graph Approach for Computing EL+-Ontology
Raisonnement automatique
Monday 15 November 2021 - 13h00
Salle : 445 - PCRI-N
Hui Yang .............................................

Semantic approaches to predict the presence of asb
Intégration de données et de connaissances
Monday 08 November 2021 - 13h00
Salle : 455 - PCRI-N
Thamer Mecharnia .............................................

Pierre Andrieu - Agrégation de classements pour le
Thursday 21 October 2021 - 00h00
Salle : 435 - PCRI-N
.............................................

A counting argument for graph colouring
Théorie des graphes
Friday 08 October 2021 - 11h00
Salle : 445 - PCRI-N
Francois Pirot .............................................