Constantinides, G;
Dahlqvist, F;
Rakamaric, Z;
Salvia, R;
(2021)
Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations.
In: Silva, A and Leino, KRM, (eds.)
(Proceedings) 33rd International Conference on Computer-Aided Verification (CAV).
(pp. pp. 626-650).
Springer
Preview |
Text
Constantinides2021_Chapter_RigorousRoundoffErrorAnalysisO.pdf - Published Version Download (1MB) | Preview |
Abstract
We present a detailed study of roundoff errors in probabilistic floating-point computations. We derive closed-form expressions for the distribution of roundoff errors associated with a random variable, and we prove that roundoff errors are generally close to being uncorrelated with their generating distribution. Based on these theoretical advances, we propose a model of IEEE floating-point arithmetic for numerical expressions with probabilistic inputs and an algorithm for evaluating this model. Our algorithm provides rigorous bounds to the output and error distributions of arithmetic expressions over random variables, evaluated in the presence of roundoff errors. It keeps track of complex dependencies between random variables using an SMT solver, and is capable of providing sound but tight probabilistic bounds to roundoff errors using symbolic affine arithmetic. We implemented the algorithm in the PAF tool, and evaluated it on FPBench, a standard benchmark suite for the analysis of roundoff errors. Our evaluation shows that PAF computes tighter bounds than current state-of-the-art on almost all benchmarks.
| Type: | Proceedings paper |
|---|---|
| Title: | Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations |
| Event: | 33rd International Conference on Computer-Aided Verification (CAV) |
| Location: | ELECTR NETWORK |
| Dates: | 20 July 2021 - 23 July 2021 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-81688-9_29 |
| Publisher version: | https://doi.org/10.1007/978-3-030-81688-9_29 |
| Language: | English |
| Additional information: | This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
| Keywords: | Science & Technology, Technology, Computer Science, Hardware & Architecture, Computer Science, Software Engineering, Computer Science, Theory & Methods, Computer Science |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10135337 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
