John Harrison: Floating Point Verification

This research project, funded by the EPSRC, aims to apply theorem proving techniques to the verification of industrially significant floating point algorithms.

The project started in September 1996. The first year's work has culminated in a major verification using HOL Light of a published algorithm for calculating the exponential function in IEEE-754 arithmetic. This is the first ever machine-checked verification of a transcendental function algorithm against a formal definition of IEEE-754. In more detail, we have:

The next stage will be to generalize this work to make it easy to verify similar algorithms quickly, and to apply it to actual designs, in cooperation with industrial partners.

You can also read the original proposal written on the 9th of February 1995. It can be seen that we are broadly ahead of the planned schedule.