IRL - Safe Floating-Point Optimisation
Safe floating-point optimisation
Satisfiability modulo theory is an approach to solving first-order formulas in certain logical theories or combinations thereof. It is used in program verification and security analyses (concolic testing), as well as for certain kinds of optimization problems.
Originally, SMT-solvers only allowed ideal arithmetic types (Z, Q), but some now also allow floating-point types. The idea is that if we wish to prove the absence of corner cases in numerical algorithms implemented with floating-point arithmetic, we must be able to specify problems with floating-point variables and floating-point operations.
One way to address this issue is to ``bit-blast floating-point operations into basic operations over bits, as in a hardware implementation of floating-point. This has been done in certain solvers (Z3\dots) but results in formulas that are very hard and slow to solve.
We instead wish to be fast in the ``easy case where a formula holds over floating-point values because it holds over the real numbers, using ideal operations, and still holds if rounding error is accounted for. For this, we will soundly take rounding error into account, with increasing precision.
The goal of this project is to explore this approach.