Formalisms for Certifying Floating-Point Algorithms
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.
KeywordsRelative Error Logical Proposition Interval Arithmetic Proof Assistant Signed Zero
Unable to display preview. Download preview PDF.