Sciweavers

ARITH
2003
IEEE

Representable Correcting Terms for Possibly Underflowing Floating Point Operations

14 years 3 months ago
Representable Correcting Terms for Possibly Underflowing Floating Point Operations
Studying floating point arithmetic, authors have shown that the implemented operations (addition, subtraction, multiplication, division and square root) can compute a result and an exact correcting term using the same format as the inputs. Following a path initiated in 1965, many authors supposed that neither underflow nor overflow occurred in the process. Overflow is not critical as this kind of exception creates persisting non numeric quantities. Underflow may be fatal to the process as it returns wrong numeric values with little warning. Our new conditions guarantee that the correcting term is exact when the result is a number. We have validated our proofs against Coq automatic proof checker. Our development has raised many questions, some of them were expected while other ones were surprising.
Sylvie Boldo, Marc Daumas
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where ARITH
Authors Sylvie Boldo, Marc Daumas
Comments (0)