Advertisement

Formalisms for Certifying Floating-Point Algorithms

  • Jean-Michel Muller
  • Nicolas Brisebarre
  • Florent de Dinechin
  • Claude-Pierre Jeannerod
  • Vincent Lefèvre
  • Guillaume Melquiond
  • Nathalie Revol
  • Damien Stehlé
  • Serge Torres
Chapter

Abstract

While the previous chapters have made clear that it is common practice to certify floating-point algorithms with pen-and-paper proofs, this practice can lead to subtle bugs. Indeed, floating-point arithmetic introduces numerous special cases, and examining all the details would be tedious. As a consequence, the certification process tends to focus on the main parts of the correctness proof, so that it does not grow out of reach.

Keywords

Relative Error Logical Proposition Interval Arithmetic Proof Assistant Signed Zero 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Birkhäuser Boston 2010

Authors and Affiliations

  • Jean-Michel Muller
    • 1
  • Nicolas Brisebarre
    • 1
  • Florent de Dinechin
    • 2
  • Claude-Pierre Jeannerod
    • 3
  • Vincent Lefèvre
    • 3
  • Guillaume Melquiond
    • 4
  • Nathalie Revol
    • 3
  • Damien Stehlé
    • 5
  • Serge Torres
    • 2
  1. 1.CNRS, Laboratoire LIPÉcole Normale Supérieure de LyonLyon Cedex 07France
  2. 2.ENSL, Laboratoire LIPÉcole Normale Supérieure de LyonLyon Cedex 07France
  3. 3.INRIA, Laboratoire LIPÉcole Normale Supérieure de LyonLyon Cedex 07France
  4. 4.INRIA Saclay – Île-de- FranceParc Orsay UniversitéOrsay CedexFrance
  5. 5.CNRSMacquarie University, and University of Sydney School of Mathematics and Statistics University of SydneySydneyAustralia

Personalised recommendations