Simic, Stella (2022) Bit-precise Verification of Numerical Properties in Fixed-point Programs. Advisor: Tribastone, Prof. Mirco. Coadvisor: Inverso, Dr. Omar . pp. 163. [IMT PhD Thesis]
![[img]](http://e-theses.imtlucca.it/style/images/fileicons/text.png) |
Text (Doctoral thesis)
Simic_phdthesis.pdf - Published Version Available under License Creative Commons Attribution Non-commercial Share Alike. Download (855kB) |
Abstract
Numerical software is prone to inaccuracies due to the finite representation of numbers. These inaccuracies propagate, possibly non-linearly, throughout the statements of a program, making it hard to predict the accumulated errors. Moreover, in programs that contain control structures, numerical errors can affect the control flow. As a result of these inaccuracies, reachability, and thus safety, may be altered with respect to the intended infinite-precision computation. This thesis considers programs that use fixed-point arithmetic to compute over non-integer quantities in finite precision. We first define a semantics of fixed-point operations in terms of operations over bit-vectors. The proposed semantics generalizes current attempts to a standardization of fixedpoint arithmetic. We then consider the problem of bit-precise numerical accuracy certification of fixed-point programs with control structures and arithmetic over variables of arbitrary, mixed precision and possibly non-deterministic value. By applying a set of parametrized transformation rules based on computable expressions for the errors incurred by single program statements, we reduce the problem of assessing whether a fixed-point program can exceed a given error bound to a reachability problem in a bit-vector program. We present an experimental evaluation of the certification technique, implemented in a prototype analyzer in a bounded model checking-based verification workflow. Our experiments on a set of fixed-point arithmetic routines commonly used in the industry show that the proposed technique can successfully certify numerical errors and can do so bitprecisely, making it the only such verification technique.
| Item Type: | IMT PhD Thesis |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| PhD Course: | Computer science and systems engineering |
| Identification Number: | https://doi.org/10.13118/imtlucca/e-theses/365/ |
| NBN Number: | urn:nbn:it:imtlucca-28388 |
| Date Deposited: | 29 Jul 2022 07:45 |
| URI: | http://e-theses.imtlucca.it/id/eprint/365 |
Actions (login required, only for staff repository)
 |
View Item |
