Elsevier Computer Arithmetic and Formal Proofs - Coq System

Floating-point arithmetic is a fundamental part of modern computing, serving as the primary method for approximating real numbers. However, because of its limited range and precision, using these algorithms can lead to unexpected failures. This book offers a way to increase confidence in floating-point software through computer-assisted verification of correctness proofs. This text provides a comprehensive view of how to formally specify and verify complex floating-point algorithms using the Coq proof assistant. Readers will learn about the Flocq formalization of floating-point arithmetic and various methods used to automate the verification process. It is an essential resource for those working in computer engineering and formal methods who need to ensure the reliability of numerical software.