Fran├žais Anglais
Accueil Annuaire Plan du site
Accueil > Evenements > Séminaires
Séminaire d'équipe(s) Verification of Algorithms, Languages and Systems
Formal Proofs of Rounding Error Bounds
Pierre Roux

27 March 2015, 10:00 - 27 March 2015, 11:30
Salle/Bat : 435/PCRI-N
Contact :

Activités de recherche : Formalisation and Proof of Numerical Programs

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
A counting argument for graph colouring
Graph Theory
Friday 08 October 2021 - 11:00
Salle : 445 - PCRI-N
Francois Pirot .............................................

Demographic reconstruction from paleogenomes of th
Thursday 25 February 2021 - 14:00
Salle : 435 - PCRI-N
Nina Marchi .............................................

A Graph-based Similarity Approach to Classify Recu
Thursday 18 February 2021 - 14:00
Salle : 435 - PCRI-N
Coline Gianfrotta .............................................

"Answer Set Programming for computing constraints-
Thursday 04 February 2021 - 14:00
Salle : 435 - PCRI-N
Maxime Mahout .............................................

"Pand├Žsim: An Epidemic Spreading Stochastic Simula
Thursday 14 January 2021 - 14:00
Salle : 435 - PCRI-N
Patrick Amar .............................................