Bit-Precise Verification of Discontinuity Errors Under Fixed-Point Arithmetic

Non-integer arithmetic is prone to numerical errors due to the finite representation of numbers. These errors propagate, possibly non-linearly, throughout the variables of a program and can affect its control flow, altering reachability, and thus safety. We consider the problem of rigorous bit-precise numerical accuracy certification of programs in the presence of control structures and operations under fixed-point arithmetic over (non-deterministic) variables of arbitrary, mixed precision. By applying program transformation, we reduce the problem of assessing whether a given error bound can be exceeded in the initial program to a reachability problem in a bit-vector program. We implement our technique as a pre-processing module that integrates seamlessly with an existing mature BMC-based verification workflow. We present an experimental evaluation of our error certification technique on a set of arithmetic routines commonly used in the industry.