Master's Thesis

Numerical algorithms are most efficiently executed using hardware floating point numbers. Thanks to the IEEE 754 standard, round-off errors are exactly specified and therefore amenable to formal verification. Multiple precision floating point libraries allow to program and reason on a relatively abstract level. If based on hardware floating point numbers, the implementation can be very efficient.

Starting from the existing formalization of IEEE floating point numbers in the AFP, the goal of this thesis is to implement and verify a multiple precision floating point arithmetic library in Isabelle/HOL.


Fabian Immler
Prof. Tobias Nipkow