Computer Arithmetic and Formal Proofs: Verifying Floating-Point Algorithms with the Coq System

ISBN-13: 9781785481123 / Angielski / Twarda / 2017 / 326 str.

Sylvie Boldo; Guillaume Melquiond

Opis

Computer Arithmetic and Formal Proofs: Floating-point Algorithms with the Coq System explores floating-point arithmetic, a tool that is ubiquitous in modern computing as the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and cause numerous failures. This book explains how to avoid this and increase confidence in floating-point software by using the computer-assisted verification of correctness proof (the Coq proof assistant), the tool that is comprehensively discussed throughout this book.

• 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

Spis treści

1. Floating-Point Arithmetic2. The Coq System3. Formalization of Formats and Basic Operators4. Automated Methods5. Error-Free Computations and Applications6. Example Proofs of Advanced Operators7. Compilation of FP Programs8. Deductive Program Verification9. Real and Numerical Analysis

O autorze

Sylvie Boldo is a Research Director at INRIA in Orsay, France. Guillaume Melquiond is a Researcher at INRIA in Orsay, France.