Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system / (Record no. 247492)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03882cam a2200649Ii 4500 |
| 001 - CONTROL NUMBER | |
| control field | on1012400060 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20190328114817.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS | |
| fixed length control field | m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr cnu|||unuuu |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 171120s2017 enk ob 001 0 eng d |
| 040 ## - CATALOGING SOURCE | |
| Original cataloging agency | N$T |
| Language of cataloging | eng |
| Description conventions | rda |
| -- | pn |
| Transcribing agency | N$T |
| Modifying agency | N$T |
| -- | IDEBK |
| -- | EBLCP |
| -- | YDX |
| -- | OPELS |
| -- | UAB |
| -- | D6H |
| -- | SNK |
| -- | OCLCF |
| -- | OCLCQ |
| -- | EZ9 |
| -- | COD |
| -- | OCLCQ |
| -- | U3W |
| -- | LVT |
| -- | MERER |
| -- | OCLCQ |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9780081011706 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 0081011709 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781785481123 |
| 035 ## - SYSTEM CONTROL NUMBER | |
| System control number | (OCoLC)1012400060 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.9.C62 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 013000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 014000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 018000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 067000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 032000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 037000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 052000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | MAT |
| Subject category code subdivision | 008000 |
| Source | bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 004.01/51 |
| Edition number | 23 |
| 100 1# - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Boldo, Sylvie, |
| Relator term | author. |
| 245 10 - TITLE STATEMENT | |
| Title | Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system / |
| Medium | [electronic resource] |
| Statement of responsibility, etc. | Sylvie Boldo, Guillaume Melquiond. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE | |
| Place of production, publication, distribution, manufacture | London : |
| Name of producer, publisher, distributor, manufacturer | ISTE Press ; |
| Place of production, publication, distribution, manufacture | Oxford, UK : |
| Name of producer, publisher, distributor, manufacturer | Elsevier, |
| Date of production, publication, distribution, manufacture, or copyright notice | 2017. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | 1 online resource |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Content type code | txt |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | computer |
| Media type code | c |
| Source | rdamedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Carrier type code | cr |
| Source | rdacarrier |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE | |
| Bibliography, etc | Includes bibliographical references and index. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | 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. |
| 588 0# - SOURCE OF DESCRIPTION NOTE | |
| Source of description note | Vendor-supplied metadata. |
| 630 00 - SUBJECT ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | Coq (Electronic resource) |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer arithmetic. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Floating-point arithmetic. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer algorithms. |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Computer Literacy. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Computer Science. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Data Processing. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Hardware |
| -- | General. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Information Technology. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Machine Theory. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | COMPUTERS |
| General subdivision | Reference. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | MATHEMATICS |
| General subdivision | Discrete Mathematics. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer algorithms. |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst00872010 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer arithmetic. |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst00872029 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Floating-point arithmetic. |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst00927429 |
| 655 #4 - INDEX TERM--GENRE/FORM | |
| Genre/form data or focus term | Electronic books. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Melquiond, Guillaume, |
| Relator term | author. |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Print version: |
| Main entry heading | Boldo, Sylvie. |
| Title | Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system. |
| Place, publisher, and date of publication | London, England ; ISTE Press : Elsevier, �2017 |
| Physical description | xx, 306 pages |
| International Standard Book Number | 9781785481123 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Materials specified | ScienceDirect |
| Uniform Resource Identifier | https://www.sciencedirect.com/science/book/9781785481123 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Materials specified | ScienceDirect |
| Uniform Resource Identifier | http://www.sciencedirect.com/science/book/9781785481123 |
No items available.