Paper Info
Title
Pitfalls of a full floating-point proof: example on the formal proof of the veltkamp/dekker algorithms
Abstract
Some floating-point algorithms have been used for decades and proved decades ago in radix-2, providing neither Underflow, nor Overflow occurs. This includes the Veltkamp algorithm, used to split a float into an upper part and a lower part and the Dekker algorithm, used to compute the exact error of a floating-point multiplication. The aim of this article is to show the difficulties of a strong justification of the validity of these algorithms for a generic radix and even when Underflow or Overflow occurs. These cases are usually dismissed even if they should not: the main argument in radix 2 of the first algorithm fails in other radices. Nevertheless all results still hold here under mild assumptions. The proof path is interesting as these cases are hardly looked into and new methods and results had to be developed.
Year
DOI
Venue
2006
10.1007/11814771_6
IJCAR
Keywords
Field
DocType
formal proof,full floating-point proof,veltkamp algorithm,exact error,floating-point multiplication,main argument,lower part,dekker algorithm,upper part,generic radix,floating-point algorithm,mild assumption,floating point
Arithmetic underflow,Computer science,Floating point,Algorithm,Proof theory,Multiplication,Formal methods,Calculus,Formal proof,Formal verification,Proof assistant
Conference
ISBN
Citations 
PageRank 
3-540-37187-7
6
0.74
References 
Authors
14
1
Name
Order
Citations
PageRank
Sylvie Boldo129226.85