The Coq mailing list

[Sylvie Boldo <sylvie.boldo AT inria.fr>]

Hello,

We are very pleased to announce the recent publication of our book 
"Computer Arithmetic and Formal Proofs: Verifying Floating-point 
Algorithms with the Coq System" (authors: Sylvie Boldo and Guillaume 
Melquiond, 326 pages, ISTE press -- Elsevier).

http://iste.co.uk/book.php?id=1238


Abstract:
Floating-point arithmetic is ubiquitous in modern computing, as it is 
the tool of choice to approximate real numbers. Due to its limited range 
and precision, its use can become quite involved and potentially lead to 
numerous failures. One way to greatly increase confidence in 
floating-point software is by computer-assisted verification of its 
correctness proofs.

This book provides a comprehensive view of how to formally specify and 
verify tricky floating-point algorithms with the Coq proof assistant. It 
describes the Flocq formalization of floating-point arithmetic and some 
methods to automate theorem proofs. It then presents the specification 
and verification of various algorithms, from error-free transformations 
to a numerical scheme for a partial differential equation. The examples 
cover not only mathematical algorithms but also C programs as well as 
issues related to compilation.

Best regards,

S. Boldo and G. Melquiond