Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Library for Symbolic Floating-Point Arithmetic

Claude-Pierre Jeannerod 1, 2 Nicolas Louvet 1, 2 Jean-Michel Muller 1, 2 Antoine Plet 1, 2 
1 ARIC - Arithmetic and Computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : To analyze a priori the accuracy of an algorithm in oating-point arithmetic, one usually derives a uniform error bound on the output, valid for most inputs and parametrized by the precision p. To show further that this bound is sharp, a common way is to build an input example for which the error committed by the algorithm comes close to that bound, or even attains it. Such inputs may be given as oating-point numbers in one of the IEEE standard formats (say, for p = 53) or, more generally, as expressions parametrized by p, that can be viewed as symbolic oating-point numbers. With such inputs, a sharpness result can thus be established for virtually all reasonable formats instead of just one of them. This, however, requires the ability to run the algorithm on those inputs and, in particular, to compute the correctly-rounded sum, product, or ratio of two symbolic oating-point numbers. The goal of this paper is to show how these basic arithmetic operations can be performed automatically. We introduce a way to model symbolic oating-point data, and present algorithms for round-to-nearest addition, multiplication, fused multiply-add, and division. An implementation as a Maple library is also described, and experiments using examples from the literature are provided to illustrate its interest in practice.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Nicolas Louvet Connect in order to contact the contributor
Submitted on : Wednesday, August 3, 2016 - 8:41:37 PM
Last modification on : Monday, May 16, 2022 - 4:58:02 PM


Files produced by the author(s)


  • HAL Id : hal-01232159, version 2



Claude-Pierre Jeannerod, Nicolas Louvet, Jean-Michel Muller, Antoine Plet. A Library for Symbolic Floating-Point Arithmetic. 2016. ⟨hal-01232159v2⟩



Record views


Files downloads