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.