Optimal Inverse Projection of Floating-Point Addition
| Autor: | Pascal Cuoq, Diane Gallois-Wong, Sylvie Boldo |
|---|---|
| Přispěvatelé: | Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), TrustInSoft (TIS ) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Floating point
Applied Mathematics Computation Numerical analysis [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 010103 numerical & computational mathematics Abstract interpretation 01 natural sciences Inverse projection IEEE floating point 010101 applied mathematics Theory of computation Local consistency Applied mathematics 0101 mathematics Mathematics |
| Zdroj: | Numerical Algorithms Numerical Algorithms, Springer Verlag, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩ Numerical Algorithms, inPress, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩ |
| ISSN: | 1017-1398 1572-9265 |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink