Computer arithmetic and formal proofs: verifying floating-point algorithms with the Coq system

摘要

The audience for this superlatively researched and crafted book includes postgraduate students and practitioners of floating-point (FP) computation or formal verification. The authors "sincerely hope that, after reading this book, you will feel like formally verifying your own floating-point algorithms." Well, I've felt like it all my computing life, but this is the first time that I'll soon dare to do so, with the substantial knowledge and confidence that this authoritative book imparts. (I say this as no stranger to formal methods, but formalizing floating-point computations is where I heretofore have not dared tread.) The Coq [1,2] higher-order logic environment and interactive proof assistant, enhanced by the floqc library that formalizes floating-point arithmetic operations and the Coqueliquot real analysis library (used for numerical analysis), are the main formal methods that underlie this work. These Coq libraries are substantially the work of the (senior) authors, and this book is (also) a high-level guide to their use.