Conference Proceedings

Optimal Bounds for Floating-Point Addition in Constant Time

Mak Andrlon, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Proceedings of the 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH) | IEEE | Published : 2019


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 pr..

View full abstract