### 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 | |

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/ |

### Conference

Conference | IEEE Symposium on Computer Arithmetic 2019 |
---|---|

Abbreviated title | ARITH 2019 |

Country | Japan |

City | Kyoto |

Period | 10/06/19 → 12/06/19 |

Internet address |

### Keywords

- addition
- arbitrary radix
- bound analysis
- floating point arithmetic

### Cite this

*Proceedings - 26th IEEE Symposium on Computer Arithmetic, ARITH-26 (2019)*(pp. 159-166). [8877445] IEEE, Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ARITH.2019.00038