Skip to Main content Skip to Navigation
Journal articles

Optimal Inverse Projection of Floating-Point Addition

Diane Gallois-Wong 1 Sylvie Boldo 1 Pascal Cuoq 2
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LRI - Laboratoire de Recherche en Informatique
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.
Complete list of metadatas

https://hal.inria.fr/hal-01939097
Contributor : Sylvie Boldo <>
Submitted on : Thursday, November 29, 2018 - 11:04:24 AM
Last modification on : Monday, January 18, 2021 - 1:52:02 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq. Optimal Inverse Projection of Floating-Point Addition. Numerical Algorithms, Springer Verlag, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩. ⟨hal-01939097⟩

Share

Metrics

Record views

182

Files downloads

331