Optimal bounds for floating-point addition in constant time

Mak Andrlon; Peter Schachte; Harald Sondergaard; Peter J. Stuckey

doi:10.1109/ARITH.2019.00038

Optimal bounds for floating-point addition in constant time

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

Department of Data Science & AI

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

1 Citation (Scopus)

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.

Original language	English
Title of host publication	Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019)
Editors	Naofumi Takagi, Sylvie Boldo, Martin Langhammer
Place of Publication	Piscataway NJ USA
Publisher	IEEE, Institute of Electrical and Electronics Engineers
Pages	159-166
Number of pages	8
ISBN (Electronic)	9781728133669
ISBN (Print)	9781728133676
DOIs	https://doi.org/10.1109/ARITH.2019.00038
Publication status	Published - 2019
Event	IEEE Symposium on Computer Arithmetic 2019 - Kyoto, Japan Duration: 10 Jun 2019 → 12 Jun 2019 Conference number: 26th http://www.lab3.kuis.kyoto-u.ac.jp/arith26/ https://ieeexplore.ieee.org/xpl/conhome/8864032/proceeding (Proceedings)

Conference

Conference	IEEE Symposium on Computer Arithmetic 2019
Abbreviated title	ARITH 2019
Country/Territory	Japan
City	Kyoto
Period	10/06/19 → 12/06/19
Internet address	http://www.lab3.kuis.kyoto-u.ac.jp/arith26/ https://ieeexplore.ieee.org/xpl/conhome/8864032/proceeding (Proceedings)

Keywords

addition
arbitrary radix
bound analysis
floating point arithmetic

Access to Document

10.1109/ARITH.2019.00038

Cite this

@inproceedings{8180acfc1927436baf3a63c8fd3aebd9,

title = "Optimal bounds for floating-point addition in constant time",

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.",

keywords = "addition, arbitrary radix, bound analysis, floating point arithmetic",

author = "Mak Andrlon and Peter Schachte and Harald Sondergaard and Stuckey, \{Peter J.\}",

year = "2019",

doi = "10.1109/ARITH.2019.00038",

language = "English",

isbn = "9781728133676",

pages = "159--166",

editor = "Naofumi Takagi and Sylvie Boldo and Martin Langhammer",

booktitle = "Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019)",

publisher = "IEEE, Institute of Electrical and Electronics Engineers",

address = "United States of America",

note = "IEEE Symposium on Computer Arithmetic 2019, ARITH 2019 ; Conference date: 10-06-2019 Through 12-06-2019",

url = "http://www.lab3.kuis.kyoto-u.ac.jp/arith26/, https://ieeexplore.ieee.org/xpl/conhome/8864032/proceeding",

}

Andrlon, M, Schachte, P, Sondergaard, H & Stuckey, PJ 2019, Optimal bounds for floating-point addition in constant time. in N Takagi, S Boldo & M Langhammer (eds), Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019). IEEE, Institute of Electrical and Electronics Engineers, Piscataway NJ USA, pp. 159-166, IEEE Symposium on Computer Arithmetic 2019, Kyoto, Japan, 10/06/19. https://doi.org/10.1109/ARITH.2019.00038

Optimal bounds for floating-point addition in constant time. / Andrlon, Mak; Schachte, Peter; Sondergaard, Harald et al.
Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019). ed. / Naofumi Takagi; Sylvie Boldo; Martin Langhammer. Piscataway NJ USA: IEEE, Institute of Electrical and Electronics Engineers, 2019. p. 159-166.

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Optimal bounds for floating-point addition in constant time

AU - Andrlon, Mak

AU - Schachte, Peter

AU - Sondergaard, Harald

AU - Stuckey, Peter J.

N1 - Conference code: 26th

PY - 2019

Y1 - 2019

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

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

KW - addition

KW - arbitrary radix

KW - bound analysis

KW - floating point arithmetic

UR - https://www.scopus.com/pages/publications/85074841628

U2 - 10.1109/ARITH.2019.00038

DO - 10.1109/ARITH.2019.00038

M3 - Conference Paper

AN - SCOPUS:85074841628

SN - 9781728133676

SP - 159

EP - 166

BT - Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019)

A2 - Takagi, Naofumi

A2 - Boldo, Sylvie

A2 - Langhammer, Martin

PB - IEEE, Institute of Electrical and Electronics Engineers

CY - Piscataway NJ USA

T2 - IEEE Symposium on Computer Arithmetic 2019

Y2 - 10 June 2019 through 12 June 2019

ER -

Optimal bounds for floating-point addition in constant time

Abstract

Conference

Keywords

Access to Document

Other files and links

Cite this