000 03762cam a2200541 i 4500
001 on1012400060
003 OCoLC
005 20250612155448.0
006 m o d
007 cr cnu|||unuuu
008 171120s2017 enk ob 001 0 eng d
040 _aN$T
_beng
_erda
_epn
_cN$T
_dN$T
_dIDEBK
_dEBLCP
_dYDX
_dOPELS
_dUAB
_dD6H
_dSNK
_dOCLCF
_dOCLCQ
_dEZ9
_dCOD
_dOCLCQ
_dU3W
_dLVT
_dMERER
_dOCLCQ
_dLQU
_dOCLCQ
_dS2H
_dOCLCO
_dVT2
_dOCLCQ
_dOCLCO
_dK6U
_dOCLCQ
_dSFB
_dOCL
_dOCLCQ
_dOCLCO
_dOCLCL
_dSXB
_dOCLCQ
_dOCLCO
019 _a1105194898
_a1105574041
_a1141933980
_a1235832973
020 _a9780081011706
_q(electronic bk.)
020 _a0081011709
_q(electronic bk.)
020 _a1785481126
_q(hbk.)
020 _a9781785481123
020 _z9781785481123
035 _a(OCoLC)1012400060
_z(OCoLC)1105194898
_z(OCoLC)1105574041
_z(OCoLC)1141933980
_z(OCoLC)1235832973
050 4 _aQA76.9.C62
072 7 _aCOM
_x013000
_2bisacsh
072 7 _aCOM
_x014000
_2bisacsh
072 7 _aCOM
_x018000
_2bisacsh
072 7 _aCOM
_x067000
_2bisacsh
072 7 _aCOM
_x032000
_2bisacsh
072 7 _aCOM
_x037000
_2bisacsh
072 7 _aCOM
_x052000
_2bisacsh
072 7 _aMAT
_x008000
_2bisacsh
082 0 4 _a004.01/51
_223
100 1 _aBoldo, Sylvie,
_eauthor.
_1https://id.oclc.org/worldcat/entity/E39PBJxhjHPrYg9f68v3hVfcyd
_934008
245 1 0 _aComputer arithmetic and formal proofs :
_bverifying floating-point algorithms with the Coq system /
_cSylvie Boldo, Guillaume Melquiond.
264 1 _aLondon :
_bISTE Press ;
_aOxford, UK :
_bElsevier,
_c2017.
300 _a1 online resource
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
504 _aIncludes bibliographical references and index.
520 _aFloating-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.
588 0 _aVendor-supplied metadata.
630 0 0 _aCoq (Electronic resource)
_934009
650 0 _aComputer arithmetic.
_934010
650 0 _aFloating-point arithmetic.
_934011
650 0 _aComputer algorithms.
700 1 _aMelquiond, Guillaume,
_eauthor.
_1https://id.oclc.org/worldcat/entity/E39PCjthBhf6wGtTxq7mHx8P73
_934012
758 _ihas work:
_aComputer arithmetic and formal proofs (Text)
_1https://id.oclc.org/worldcat/entity/E39PCFTQ4D7qCgmFRDdjbVmYWC
_4https://id.oclc.org/worldcat/ontology/hasWork
776 0 8 _iPrint version:
_aBoldo, Sylvie.
_tComputer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system.
_dLondon, England ; ISTE Press : Elsevier, �2017
_hxx, 306 pages
_z9781785481123
856 4 0 _3ScienceDirect
_uhttps://www.sciencedirect.com/science/book/9781785481123
999 _c216417
_d216417