Name
Abstract | ||
|---|---|---|
Reasoning about floating-point numbers is notoriously difficult, owing to the lack of convenient algebraic properties such as associativity. This poses a substantial challenge for program analysis and verification tools which rely on precise floating-point constraint solving. Currently, interval methods in this domain often exhibit slow convergence even on simple examples. We present a new theorem supporting efficient computation of exact bounds of the intersection of a rectangle with the preimage of an interval under floating-point addition, in any radix or rounding mode. We thus give an efficient method of deducing optimal bounds on the components of an addition, solving the convergence problem. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1109/ARITH.2019.00038 | 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH) |
Keywords | Field | DocType |
floating point arithmetic,addition,bound analysis,arbitrary radix | Convergence (routing),Applied mathematics,Associative property,Computer science,Floating point,Rectangle,Convergence problem,Theoretical computer science,Rounding,Image (mathematics),Program analysis | Conference |
ISSN | ISBN | Citations |
1063-6889 | 978-1-7281-3367-6 | 0 |
PageRank | References | Authors |
0.34 | 5 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mak Andrlon | 1 | 0 | 0.34 |
| Peter Schachte | 2 | 256 | 22.76 |
| Harald Søndergaard | 3 | 0 | 0.34 |
| Peter J. Stuckey | 4 | 4368 | 457.58 |