Validation of a Formal Floating-Point Model

Calculations with real numbers are commonly approximated by floating-point arithmetic in computers. A floating-point number is represented by a fixed number of bits. Arithmetic operations, such as addition or multiplication, return a rounded result when the precise result of the operation cannot be represented as a floating-point number with the given (limited) precision. The precise behavior of floating-point operations is specified by the IEEE Standard for Floating-Point Arithmetic.

Floating-point arithmetic is often implemented in dedicated hardware accelerators, but can also be implemented in software. The interactive proof assistant Isabelle offers an implementation of floating-point arithmetic in formal logic. This facilitates reasoning about the behavior of floating-point operations; for instance, to prove that x+y = y+x for all floating-point numbers x and y (where + denotes floating-point addition).

The goal of this project is to test this formal model of floating-point arithmetic, using given test vectors, to determine whether it correctly implements the IEEE floating-point semantics. In other words, we want to find out whether the operations that the model defines behave as required by the IEEE standard.

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:
C++/Make/shell scripts, Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Floating-point arithmetic, software testing, first-order logic
Tjark Weber

Last modified: 2023-11-06