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.
- 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