
Computer Arithmetic and Formal Proofs
Verifying Floating-point Algorithms with the Coq System
Description
Key Features
- Describes the notions of specification and weakest precondition computation and their practical use
- Shows how to tackle algorithms that extend beyond the realm of simple floating-point arithmetic
- Includes real analysis and a case study about numerical analysis
Readership
Table of Contents
1. Floating-Point Arithmetic
2. The Coq System
3. Formalization of Formats and Basic Operators
4. Automated Methods
5. Error-Free Computations and Applications
6. Example Proofs of Advanced Operators
7. Compilation of FP Programs
8. Deductive Program Verification
9. Real and Numerical Analysis
Product details
- No. of pages: 326
- Language: English
- Copyright: © ISTE Press - Elsevier 2017
- Published: November 16, 2017
- Imprint: ISTE Press - Elsevier
- Hardcover ISBN: 9781785481123
- eBook ISBN: 9780081011706
About the Authors
Sylvie Boldo
Affiliations and Expertise
Guillaume Melquiond
Affiliations and Expertise
Ratings and Reviews
Latest reviews
(Total rating for all reviews)
SamuelPollard Wed Mar 25 2020
Comprehensive floating point formalization
This is a great project. The book describes the motivation behind how exactly to formalize floating point numbers in Coq. For those not familiar with Coq, there is a brief introduction, but this book is not complete introduction to Coq. The style is slightly in the literate-programming style, but with mostly complete definitions (some are simplified for purposes of exposition), and with proofs elided. The first three chapters describe Coq, floating point, and the Flocq basics, and the rest of the book describes applications of Flocq. This, paired with "Handbook of floating point arithmetic, 2nd edition" has all you need to know about floating point arithmetic. The book includes many informal proofs of the important results and explains the overall structure of the formal proofs, but the formal proofs are complex and difficult to follow (looking at the Flocq source code). There is relatively little proof automation in the source code which, with my limited experience in Coq, means I've struggled expanding and using Flocq. This is not so much a criticism of this book but rather of the challenges just starting to be addressed with the new field of proof engineering.