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

Numerical software is prone to inaccuracies due to the fi- nite representation of numbers. These inaccuracies propa- gate, possibly non-linearly, throughout the statements of a program, making it hard to predict the accumulated errors. Moreover, in programs that contain control structures, nu- merical 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 arith- metic to compute over non-integer quantities in finite pre- cision. We first define a semantics of fixed-point operations in terms of operations over bit-vectors. The proposed seman- tics generalizes current attempts to a standardization of fixed- point 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 sin- gle program statements, we reduce the problem of assess- ing whether a fixed-point program can exceed a given er- ror bound to a reachability problem in a bit-vector pro- gram. We present an experimental evaluation of the certifi- cation technique, implemented in a prototype analyzer in a bounded model checking-based verification workflow. Our experiments on a set of fixed-point arithmetic routines com- monly used in the industry show that the proposed technique can successfully certify numerical errors and can do so bit- precisely, making it the only such verification technique.