{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T16:27:07Z","timestamp":1780936027341,"version":"3.54.1"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,8,21]],"date-time":"2015-08-21T00:00:00Z","timestamp":1440115200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s10817-015-9339-z","type":"journal-article","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:41:28Z","timestamp":1440060088000},"page":"135-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Formal Proofs of Rounding Error Bounds"],"prefix":"10.1007","volume":"57","author":[{"given":"Pierre","family":"Roux","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"9339_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development : Coq\u2019Art : the calculus of inductive constructions. Texts in theoretical computer science","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P., Huet, G., Paulin-Mohring, C.: Interactive theorem proving and program development : Coq\u2019Art : the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin (2004). Donn\u00e9es compl\u00e9mentaires http:\/\/coq.inria.fr"},{"key":"9339_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs, volume 5170 of Lecture Notes in Computer Science, pp. 86\u2013101. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9339_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: The method error. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pp. 147\u2013162. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_12"},{"key":"9339_CR4","volume-title":"Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pp. 243\u2013252","author":"S Boldo","year":"2011","unstructured":"Boldo, S., Melquiond, G.: Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. In: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pp. 243\u2013252. T\u00fcbingen, Germany (2011)"},{"key":"9339_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Construction of real algebraic numbers in coq. In: Beringer, L., Felty, A.P. (eds.) ITP, volume 7406 of Lecture Notes in Computer Science, pp. 67\u201382. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"9339_CR6","unstructured":"The Coq development team: The Coq proof assistant reference manual. Version 8.4 (2012)"},{"key":"9339_CR7","doi-asserted-by":"crossref","unstructured":"de Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: Haddad, H. (ed.) Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), Dijon, France, April 23-27, 2006, pp. 1318\u20131322. ACM (2006)","DOI":"10.1145\/1141277.1141584"},{"key":"9339_CR8","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, INRIA (2008)"},{"key":"9339_CR9","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Floating point verification in HOL. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, volume 971 of Lecture Notes in Computer Science, pp. 186\u2013199. Springer (1995)","DOI":"10.1007\/3-540-60275-5_65"},{"key":"9339_CR10","unstructured":"Higham, N.: Accuracy and Stability of Numerical Algorithms. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA (1996)"},{"key":"9339_CR11","unstructured":"IEEE Computer Society: IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754-2008 (2008)"},{"key":"9339_CR12","doi-asserted-by":"crossref","unstructured":"Roux, P., Garoche, P.-L.: Computing quadratic invariants with min- and max-policy iterations: A practical comparison. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pp. 563\u2013578. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_38"},{"key":"9339_CR13","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"S Rump","year":"2006","unstructured":"Rump, S.: Verification of positive definiteness. BIT Numer. Math. 46, 433\u2013452 (2006)","journal-title":"BIT Numer. Math."},{"key":"9339_CR14","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S096249291000005X","volume":"19","author":"S Rump","year":"2010","unstructured":"Rump, S.: Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica 19, 287\u2013449 (2010)","journal-title":"Acta Numerica"},{"issue":"2","key":"9339_CR15","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1137\/130927231","volume":"35","author":"S Rump","year":"2014","unstructured":"Rump, S., Jeannerod, C.P.: Improved backward error bounds for lu and cholesky factorizations. SIAM J. Matrix Anal. Appl. 35(2), 684\u2013698 (2014)","journal-title":"SIAM J. Matrix Anal. Appl."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9339-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9339-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9339-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T12:42:39Z","timestamp":1567082559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9339-z"}},"subtitle":["With Application to an Automatic Positive Definiteness Check"],"short-title":[],"issued":{"date-parts":[[2015,8,21]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["9339"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9339-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,21]]}}}