A Branch-and-bound Algorithm to Rigorously Enclose the Round-Off Errors

1Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Round-off errors occur each time a program makes use of floating-point computations. They denote the existence of a distance between the actual floating-point computations and the intended computations over the reals. Therefore, analyzing round-off errors is a key issue in the verification of programs with floating-point computations. Most existing tools for round-off error analysis provide an over-approximation of the error. The point is that these approximations are often too coarse to evaluate the effective consequences of the error on the behaviour of a program. Some other tools compute an under-approximation of the maximal error. But these under-approximations are either not rigorous or not reachable. In this paper, we introduce a branch-and-bound algorithm to rigorously enclose the maximal error. Thanks to the use of rational arithmetic, our branch-and-bound algorithm provides a tight upper bound of the maximal error and a lower bound that can be exercised by input values. We outline the advantages and limits of our framework and compare it with state-of-the-art methods. Preliminary experiments on standard benchmarks show promising results.

Cite

CITATION STYLE

APA

Garcia, R., Michel, C., & Rueher, M. (2020). A Branch-and-bound Algorithm to Rigorously Enclose the Round-Off Errors. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12333 LNCS, pp. 637–653). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-58475-7_37

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free