nach oben

Numerical Algorithms

Erschienen in:

24.05.2019 | Original Paper

Optimal inverse projection of floating-point addition

verfasst von: Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq

Erschienen in: Numerical Algorithms | Ausgabe 3/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In a setting where we have intervals for the values of floating-point variables x, a, and b, we are interested in improving these intervals when the floating-point equality x ⊕ a = b holds. This problem is common in constraint propagation and called the inverse projection of the addition. It also appears in abstract interpretation for the analysis of programs containing IEEE 754 operations. We propose floating-point theorems that provide optimal bounds for all the intervals. Fast loop-free algorithms compute these optimal bounds using only floating-point computations at the target precision.

Vorheriger Artikel Error bounds for linear complementarity problems of S-QN matrices

Nächster Artikel A computational approach for the non-smooth solution of non-linear weakly singular Volterra integral equation with proportional delay

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Note that designing interval arithmetic operations to work with infinite bounds requires special care, but is not impossible.

One example is x ∈[0x1.00068db8bac72p + 0,2.0], a ∈[0x1.000d1b71758e2p + 0,2.0] and b = 0x1.fff2e53a4e1dbp− 1. The operation 0x1.00068db8bac72p + 0 / 0x1.000d1b71758e2p + 0 evaluates to 0x1.fff2e53a4e1dcp− 1, whereas 0x1.00068db8bac72p + 0 / 0x1.000d1b71758e3p + 0 evaluates to 0x1.fff2e53a4e1dap− 1, and 0x1.00068db8bac73p + 0 / 0x1.000d1b71758e3p + 0 evaluates to 0x1.fff2e53a4e1dcp− 1 again, and so on.

Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Software Testing Verification and Reliability 16(2), 97–121 (2006). https://doi.org/10.1002/stvr.333 CrossRef

Chen, L., Miné, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) Programming Languages and Systems, pp 3–18. Springer, Berlin (2008)CrossRef

Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp 106–130. Dunod, Paris, France (1976)

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Sethi, R. (ed.) Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp 238–252. ACM, Los Angeles, CA, USA (1977), https://doi.org/10.1145/512950.512973

IEEE Computer Society: IEEE standard for floating-point arithmetic. Tech. Rep. 754-2008. https://doi.org/10.1109/IEEESTD.2008.4610935 (2008)

ISO: International standard ISO/IEC 9899:2011 Programming languages – C (2011)

Marre, B., Michel, C.: Improving the floating point addition and subtraction constraints. In: Cohen, D. (ed.) Principles and Practice of Constraint Programming – CP 2010, pp 360–367. Springer, Berlin (2010)CrossRef

Michel, C.: Exact projection functions for floating point number constraints. In: International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida, USA (2002). Http://Rutcor.Rutgers.Edu/ Amai/Aimath02/PAPERS/21.Ps. (AI&m (2002)

Michel, C., Rueher, M., Lebbah, Y.: Solving constraints over floating-point numbers. In: Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, CP ’01, pp 524–538. Springer, London (2001). http://dl.acm.org/citation.cfm?id=647488.726803 CrossRef

10.

Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) Programming Languages and Systems, pp 3–17. Springer, Berlin (2004)

11.

Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30(3), 1–41 (2008). https://doi.org/10.1145/1353445.1353446 CrossRef

12.

Moore, R.E.: Interval analysis. Prentice-Hall, Englewood Cliffs (1963)

13.

Muller, J.M.: On the definition of ulp(x). Tech. Rep. RR-5504, INRIA. https://hal.inria.fr/inria-00070503 (2005)

14.

Rump, S.M., Zimmermann, P., Boldo, S., Melquiond, G.: Computing predecessor and successor in rounding to nearest. BIT 49(2), 419–431 (2009). https://doi.org/10.1007/s10543-009-0218-z. http://hal.inria.fr/inria-00337537/fr/ MathSciNetCrossRef

15.

Sterbenz, P.H.: Floating point computation. Prentice Hall (1974)

Titel: Optimal inverse projection of floating-point addition
verfasst von: Diane Gallois-Wong
Sylvie Boldo
Pascal Cuoq
Publikationsdatum: 24.05.2019
Verlag: Springer US
Erschienen in: Numerical Algorithms / Ausgabe 3/2020
Print ISSN: 1017-1398
Elektronische ISSN: 1572-9265
DOI: https://doi.org/10.1007/s11075-019-00711-z

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Weitere Artikel der Ausgabe 3/2020

How to compute the minimum norm least squares solution of singular linear system by using the preconditioned HSS method?

A computational approach for the non-smooth solution of non-linear weakly singular Volterra integral equation with proportional delay

Sharp H1-norm error estimate of a cosine pseudo-spectral scheme for 2D reaction-subdiffusion equations

The dynamical analysis of a uniparametric family of three-point optimal eighth-order multiple-root finders under the Möbius conjugacy map on the Riemann sphere

A new coarse space for overlapping Schwarz algorithms for H(curl) problems in three dimensions with irregular subdomains

An augmented Lagrangian proximal alternating method for sparse discrete optimization problems