03882cam a2200649Ii 4500 on1012400060 OCoLC 20190328114817.0 m o d cr cnu|||unuuu 171120s2017 enk ob 001 0 eng d N$T eng rda pn N$T N$T IDEBK EBLCP YDX OPELS UAB D6H SNK OCLCF OCLCQ EZ9 COD OCLCQ U3W LVT MERER OCLCQ 9780081011706 (electronic bk.) 0081011709 (electronic bk.) 9781785481123 (OCoLC)1012400060 QA76.9.C62 COM 013000 bisacsh COM 014000 bisacsh COM 018000 bisacsh COM 067000 bisacsh COM 032000 bisacsh COM 037000 bisacsh COM 052000 bisacsh MAT 008000 bisacsh 004.01/51 23 Boldo, Sylvie, author. Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system / [electronic resource] Sylvie Boldo, Guillaume Melquiond. London : ISTE Press ; Oxford, UK : Elsevier, 2017. 1 online resource text txt rdacontent computer c rdamedia online resource cr rdacarrier Includes bibliographical references and index. 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. Describes the notions of specification and weakest precondition computation and their practical useShows how to tackle algorithms that extend beyond the realm of simple floating-point arithmeticIncludes real analysis and a case study about numerical analysis. Vendor-supplied metadata. Coq (Electronic resource) Computer arithmetic. Floating-point arithmetic. Computer algorithms. COMPUTERS Computer Literacy. bisacsh COMPUTERS Computer Science. bisacsh COMPUTERS Data Processing. bisacsh COMPUTERS Hardware General. bisacsh COMPUTERS Information Technology. bisacsh COMPUTERS Machine Theory. bisacsh COMPUTERS Reference. bisacsh MATHEMATICS Discrete Mathematics. bisacsh Computer algorithms. fast (OCoLC)fst00872010 Computer arithmetic. fast (OCoLC)fst00872029 Floating-point arithmetic. fast (OCoLC)fst00927429 Electronic books. Melquiond, Guillaume, author. Print version: Boldo, Sylvie. Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system. London, England ; ISTE Press : Elsevier, �2017 xx, 306 pages 9781785481123 ScienceDirect https://www.sciencedirect.com/science/book/9781785481123 ScienceDirect http://www.sciencedirect.com/science/book/9781785481123 247492 247492