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).

• Philipp Rümmer, Thomas Wahl
  An SMT-LIB Theory of Binary Floating-Point Arithmetic
  (PDF - BibTeX - Abstract)
• Current textual definition of the syntax of the theory.
• We also provide a reference implementation of the floating-point datatype specified in the theory. The implementation is written in Scala 2.8 and follows closely the definitions in the workshop paper.
• A preliminary collection of conformance tests for solvers implementing the floating-point theory. Currently, this is a large collection of simple SMT-LIB 2 benchmarks that verify the semantics of the operations +, *, -, /, max, min, ==, <, <=. We will provide more benchmarks soon.

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

Solvers

The following solvers support the floating-point theory:

• Microsoft's Z3
• MathSAT 5
• CBMC's built-in solver. CBMC can also generate benchmarks for this theory.