Logo eprints

Bit-precise Verification of Numerical Properties in Fixed-point Programs

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] Text (Doctoral thesis)
Simic_phdthesis.pdf - Published Version
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (855kB)


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 View Item