Satisfiability modulo
Floating-Point Arithmetic

Floating-point arithmetic is an essential ingredient of embedded systems, such as in the avionics and automotive industries. By nature, many of these applications are safety-critical, requiring rigorous mathematical methods such as model checking to verify the adherence to safety standards. To support verification systems, we are working on decision procedures for floating-point arithmetic. More specifically, we have designed and formalised a theory of floating-point arithmetic following the SMT-LIB 2 standard. There are now at least three solvers that support the theory. We gratefully acknowledge support by a Microsoft Software Engineering Innovation Foundation Award Testing Embedded Software with the Z3 SMT Solver.

An SMT-LIB Theory of Binary Floating-Point Arithmetic

Our theory mostly follows the IEEE 754-2008 standard and covers the essential arithmetic core of IEEE floating-point arithmetic. Certain aspects, such as exceptions and error handling, are simplified compared to the IEEE standard, in order to avoid ambiguities (parts of the standard that are left implementation-specific) and to make the development of solvers feasible. The theory was presented at the SMT Workshop 2010 (at FLoC in Edinburgh, Scotland).

For feedback or questions about theory, please contact Philipp Ruemmer, Thomas Wahl and Martin Brain.


The following solvers support the floating-point theory: