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é () and Serge Torres ()
Additional contact information
Jean-Michel Muller: École Normale Supérieure de Lyon, CNRS, Laboratoire LIP
Nicolas Brisebarre: École Normale Supérieure de Lyon, CNRS, Laboratoire LIP
Florent de Dinechin: École Normale Supérieure de Lyon, ENSL, Laboratoire LIP
Claude-Pierre Jeannerod: École Normale Supérieure de Lyon, INRIA, Laboratoire LIP
Vincent Lefèvre: École Normale Supérieure de Lyon, INRIA, Laboratoire LIP
Guillaume Melquiond: Parc Orsay Université, INRIA Saclay – Île-de- France
Nathalie Revol: École Normale Supérieure de Lyon, INRIA, Laboratoire LIP
Damien Stehlé: Macquarie University, and University of Sydney School of Mathematics and Statistics University of Sydney, CNRS
Serge Torres: École Normale Supérieure de Lyon, ENSL, Laboratoire LIP

Chapter Chapter 13 in Handbook of Floating-Point Arithmetic, 2010, pp 463-491 from Springer

Abstract: 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 (search for similar items in EconPapers)
Date: 2010
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-0-8176-4705-6_13

Ordering information: This item can be ordered from
http://www.springer.com/9780817647056

DOI: 10.1007/978-0-8176-4705-6_13

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().