Paper Info
Title
Representable Correcting Terms for Possibly Underflowing Floating Point Operations
Abstract
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 manyquestions, some of them were expected while other ones were surprising.
Year
DOI
Venue
2003
10.1109/ARITH.2003.1207663
IEEE Symposium on Computer Arithmetic
Keywords
Field
DocType
representable correcting terms,floating point arithmetic,square root,non numeric quantity,coq automatic proof checker,floating point operations,new condition,wrong numeric value,theorem proving,error correction,floating point
Arithmetic underflow,Fixed-point arithmetic,Floating point,Arbitrary-precision arithmetic,Computer science,Arithmetic,Algorithm,Machine epsilon,Minifloat,Arithmetic overflow,Saturation arithmetic
Conference
ISSN
ISBN
Citations 
1063-6889
0-7695-1894-X
16
PageRank 
References 
Authors
1.56
7
2
Name
Order
Citations
PageRank
Sylvie Boldo129226.85
Marc Daumas221625.32