{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T08:08:39Z","timestamp":1776845319522,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_6","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"52-66","source":"Crossref","is-referenced-by-count":14,"title":["Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp\/Dekker Algorithms"],"prefix":"10.1007","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"252","DOI":"10.2307\/2316620","volume":"79","author":"P.J. Davis","year":"1972","unstructured":"Davis, P.J.: Fidelity in mathematical discourse: Is one and one really two? Amer. Math. Monthly\u00a079, 252\u2013263 (1972)","journal-title":"Amer. Math. Monthly"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/2455.2457","volume":"32","author":"L. Lamport","year":"1985","unstructured":"Lamport, L., Melliar-Smith, P.M.: Synchronizing clocks in the presence of faults. Journal of the ACM\u00a032(1), 52\u201378 (1985)","journal-title":"Journal of the ACM"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Rushby, J., von Henke, F.: Formal verification of algorithms for critical systems. In: Conference on Software for Critical Systems, New Orleans, Louisiana (1991)","DOI":"10.1145\/125083.123044"},{"key":"6_CR4","unstructured":"Carre\u00f1o, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah (1995) (supplemental proceedings)"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D.M. Russinoff","year":"1999","unstructured":"Russinoff, D.M.: A mechanically checked proof of correctness of the amd k5 floating point square root microcode. Formal Methods in System Design\u00a014(1), 75 (1999)","journal-title":"Formal Methods in System Design"},{"key":"6_CR6","unstructured":"Jacobi, C.: Formal Verification of a Fully IEEE Compliant Floating Point Unit. PhD thesis, Saarland University, Saarbrucken, Germany (2002)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: 12th International Conference on Theorem Proving in Higher Order Logics, Nice (1999)","DOI":"10.1007\/3-540-48256-3_9"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions. In: Hunt, W.A., Johnson, S.D. (eds.) Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, Austin, Texas, pp. 217\u2013233 (2000)","DOI":"10.1007\/3-540-40922-X_14"},{"key":"6_CR9","unstructured":"The Coq Development Team, LogiCal Project, INRIA: The Coq Proof Assistant: Reference Manual, Version 8.0 (2004)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library of floating-point numbers and its application to exact computing. In: 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 169\u2013184 (2001)","DOI":"10.1007\/3-540-44755-5_13"},{"key":"6_CR11","unstructured":"Veltkamp, G.W.: Algolprocedures voor het berekenen van een inwendig product in dubbele precisie. RC-Informatie\u00a022, Technische Hogeschool Eindhoven (1968)"},{"key":"6_CR12","unstructured":"Veltkamp, G.W.: ALGOL procedures voor het rekenen in dubbele lengte. RC-Informatie\u00a021, Technische Hogeschool Eindhoven (1969)"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/BF01397083","volume":"18","author":"T.J. Dekker","year":"1971","unstructured":"Dekker, T.J.: A floating point technique for extending the available precision. Numerische Mathematik\u00a018(3), 224\u2013242 (1971)","journal-title":"Numerische Mathematik"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Priest, D.M.: Algorithms for arbitrary precision floating point arithmetic. In: 10th Symposium on Computer Arithmetic, Grenoble, France, pp. 132\u2013144 (1991)","DOI":"10.1109\/ARITH.1991.145549"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Shewchuk, J.R.: Adaptive precision floating-point arithmetic and fast robust geometric predicates. In: Discrete and Computational Geometry, vol.\u00a018 (1997)","DOI":"10.1007\/PL00009321"},{"issue":"3","key":"6_CR16","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1109\/C-M.1981.220377","volume":"14","author":"D. Stevenson","year":"1981","unstructured":"Stevenson, D., et al.: A proposed standard for binary floating point arithmetic. IEEE Computer\u00a014(3), 51\u201362 (1981)","journal-title":"IEEE Computer"},{"issue":"2","key":"6_CR17","first-page":"9","volume":"22","author":"D. Stevenson","year":"1987","unstructured":"Stevenson, D., et al.: An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices\u00a022(2), 9\u201325 (1987)","journal-title":"ACM SIGPLAN Notices"},{"key":"6_CR18","unstructured":"Floating-Point Working Group of\u00a0the Microprocessor Standards Subcommittee of the Standards Committee of\u00a0the IEEE Computer\u00a0Society, F.P.W.G.: IEEE standard for floating-point arithmetic (2006) (Work in progress)"},{"issue":"4","key":"6_CR19","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/MM.1984.291224","volume":"4","author":"W.J. Cody","year":"1984","unstructured":"Cody, W.J., Karpinski, R., et al.: A proposed radix and word-length independent standard for floating point arithmetic. IEEE Micro.\u00a04(4), 86\u2013100 (1984)","journal-title":"IEEE Micro."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying the accuracy of polynomial approximations in HOL. In: Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, Murray Hill, New Jersey, pp. 137\u2013152 (1997)","DOI":"10.1007\/BFb0028391"},{"key":"6_CR21","unstructured":"Muller, J.M.: On the definition of ulp(x). Technical Report LIP RR2005-09 INRIA RR-5504, Laboratoire de l\u2019Informatique du Parall\u00e9lisme (2005)"},{"key":"6_CR22","volume-title":"Floating point computation","author":"P.H. Sterbenz","year":"1974","unstructured":"Sterbenz, P.H.: Floating point computation. Prentice-Hall, Englewood Cliffs (1974)"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1145\/355958.355960","volume":"7","author":"S. Linnainmaa","year":"1981","unstructured":"Linnainmaa, S.: Software for doubled-precision floating-point computations. ACM Transactions on Mathematical Software\u00a07(3), 272\u2013283 (1981)","journal-title":"ACM Transactions on Mathematical Software"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Boldo, S., Daumas, M.: Representable correcting terms for possibly underflowing floating point operations. In: Symposium on Computer Arithmetic, Spain (2003)","DOI":"10.1109\/ARITH.2003.1207663"},{"issue":"6","key":"6_CR25","doi-asserted-by":"publisher","first-page":"1955","DOI":"10.1137\/030601818","volume":"26","author":"T. Ogita","year":"2005","unstructured":"Ogita, T., Rump, S.M., Oishi, S.: Accurate sum and dot product. SIAM Journal on Scientific Computing\u00a026(6), 1955\u20131988 (2005)","journal-title":"SIAM Journal on Scientific Computing"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:39Z","timestamp":1605644079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11814771_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}