John Harrison: Floating Point Verification

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:

• Liased with industrial sites to find a realistic algorithm to tackle. Previous work, e.g. as described in John Harrison's thesis was only for rather simple algorithms such as CORDIC, and was based on an ad hoc floating point format rather than the IEEE-754 standard. As a result of industrial feedback, we selected a table-driven algorithm for the exponential function as our target.
• Developed more mathematical infrastructure in HOL to deal with reasoning about the accuracy of polynomial approximations. This includes a formalization of polynomial theory, e.g. squarefree decomposition and Sturm's theorem, and is described in a separate paper recently published in the proceedings of TPHOLs'97.
• Developed an embedding of a simple algorithm implementation language in HOL Light, based on existing work by Mike Gordon, Joakim von Wright and Tobias Nipkow.
• Formalized the IEEE-754 Standard for binary floating point arithmetic in HOL. In this endeavour, similar work on formalizing IEEE-854 standard in PVS by Paul Miner was often a helpful guide.
• Adapted and formalized the algorithm and published proof of the algorithm into HOL. The hand proof contained one error and a few missing details, but the final result has been confirmed, and in fact strengthened. The entire verification effort is described in exhaustive detail in the following paper.

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.