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

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