Monday, 21 December 2009

Formally verifying Intel's floating-point arithmetic using OCaml

When a bug in floating point division on the Pentium processor was discovered, Intel had to set aside $475,000,000 to cover the cost of replacing the faulty hardware. To minimize the risk of this happening again, Intel now formally verify their floating point hardware using theorem-proving software written in OCaml.

John Harrison of Intel has kindly made the fascinating slides from his lecture about Intel's use of OCaml freely available.

John has a new book out called the Handbook of Practical Logic and Automated Reasoning.