Formalisms for Certifying Floating-Point Algorithms

Abstract

While the previous chapters have made clear that it is common practice to certify floating-point algorithms with pen-and-paper proofs, this practice can lead to subtle bugs. Indeed, floating-point arithmetic introduces numerous special cases, and examining all the details would be tedious. As a consequence, the certification process tends to focus on the main parts of the correctness proof, so that it does not grow out of reach.