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.