Approximations for Reasoning about Floating-Point Arithmetic

Abstract:

Safety-critical systems, especially those found in avionics and automotive industries, rely on various forms of machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic, especially FPA, can exhibit subtle differences in behavior compared to the ideal mathematical arithmetic, due to fixed-size representation in memory. The price of failure of safety-critical systems can be unacceptably high, since they can cost human lives or huge amounts of money, time
and effort. To prevent such occurrences, we want to formally prove that systems satisfy certain safety properties, or otherwise discover cases when the properties are violated. To achieve this, ability to formally reason about machine arithmetic is required. The main difficulty existing approaches face is their lack of scalability with the increasing complexity of systems and their properties.

We present a general approximation refinement framework which we apply to solve constraints over floating-point arithmetic. It is built around an existing decision procedure, e.g., bit-blasting. Rather than solving the original formula, it solves a sequence of approximations of the formula, until either a model is found or the formula is determined to be unsatisfiable. Usually these type of refinement schemes use over- and under-approximations, however they are very difficult to design for floating-point arithmetic. Instead, the
framework allows use of non-conservative approximations. The presented framework is general and preserves soundness, completeness and termination of the underlying procedure. In the case of floating-point arithmetic, it improves the solving time and the number of instances
that can be solved when compared to bit-blasting alone.

Bio:

Aleksandar Zeljic is a PhD student at Department of Information Technology at Uppsala Unversity, advised by Philipp Ruemmer and Christoph Wintersteiger. His research focuses on improving scalability of SMT-style reasoning about machine arithmetic, through use of approximations and abstractions.