{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:15Z","timestamp":1776423795856,"version":"3.51.2"},"reference-count":79,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,12,6]],"date-time":"2023-12-06T00:00:00Z","timestamp":1701820800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,6]],"date-time":"2023-12-06T00:00:00Z","timestamp":1701820800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s10817-023-09686-y","type":"journal-article","created":{"date-parts":[[2023,12,6]],"date-time":"2023-12-06T19:02:03Z","timestamp":1701889323000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formally-Verified Round-Off Error Analysis of Runge\u2013Kutta Methods"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5792-0658","authenticated-orcid":false,"given":"Florian","family":"Faissole","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,6]]},"reference":[{"key":"9686_CR1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/8124","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. (2018). https:\/\/doi.org\/10.6092\/issn.1972-5787\/8124","journal-title":"J. Formaliz. Reason."},{"issue":"1","key":"9686_CR2","first-page":"1","volume":"13","author":"A Appel","year":"2020","unstructured":"Appel, A., Bertot, Y.: C floating point proofs layered with VST and Flocq. J. Formaliz. Reason. 13(1), 1\u201316 (2020)","journal-title":"J. Formaliz. Reason."},{"key":"9686_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Verified software toolchain. In: European Symposium on Programming, pp. 1\u201317. Springer (2011)","DOI":"10.1007\/978-3-642-19718-5_1"},{"issue":"7","key":"9686_CR4","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1080\/00423114.2011.582953","volume":"49","author":"M Arnold","year":"2011","unstructured":"Arnold, M., Burgermeister, B., F\u00fchrer, C., Hippmann, G., Rill, G.: Numerical methods in vehicle system dynamics: state of the art and current developments. Veh. Syst. Dyn. 49(7), 1159\u20131207 (2011)","journal-title":"Veh. Syst. Dyn."},{"key":"9686_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530074","volume-title":"Pad\u00e9 approximants","author":"GA Baker Jr","year":"1996","unstructured":"Baker, G.A., Jr., Graves-Morris, P.: Pad\u00e9 approximants, vol. 59. Cambridge University Press, Cambridge (1996)"},{"key":"9686_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Ould\u00a0Biha, S., Pa\u015fca, I.: Canonical big operators. In: Theorem Proving in Higher Order Logics, volume 5170\/2008 of Lecture Notes in Computer Science, Montreal, Canada (August 2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"issue":"4","key":"9686_CR7","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M Berz","year":"1998","unstructured":"Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliab. Comput."},{"key":"9686_CR8","doi-asserted-by":"publisher","DOI":"10.1201\/9781420011869","volume-title":"Numerical Methods in Astrophysics: An Introduction","author":"P Bodenheimer","year":"2006","unstructured":"Bodenheimer, P., Laughlin, G.P., Rozyczka, M., Plewa, T., Yorke, H.W.: Numerical Methods in Astrophysics: An Introduction. Series in Astronomy and Astrophysics. CRC Press, Boca Raton (2006)"},{"key":"9686_CR9","doi-asserted-by":"crossref","unstructured":"Bohrer, B., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 208\u2013221. ACM (2017)","DOI":"10.1145\/3018610.3018616"},{"key":"9686_CR10","doi-asserted-by":"crossref","unstructured":"Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science - ARCoSS, pp. 91\u2013102, Rhodos, Greece (July 2009). Springer","DOI":"10.1007\/978-3-642-02930-1_8"},{"issue":"4","key":"9686_CR11","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-012-9255-4","volume":"50","author":"S Boldo","year":"2013","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reason."},{"key":"9686_CR12","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax\u2013Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 79\u201389, Paris, France (January 2017). ACM","DOI":"10.1145\/3018610.3018625"},{"key":"9686_CR13","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.) Proceedings of the first Interactive Theorem Proving Conference (ITP), volume 6172 of Lecture Notes in Computer Science, pp. 147\u2013162, Edinburgh, Scotland (July 2010). Springer. (merge of TPHOL and ACL2)","DOI":"10.1007\/978-3-642-14052-5_12"},{"key":"9686_CR14","doi-asserted-by":"publisher","first-page":"1745","DOI":"10.1109\/TC.2019.2917902","volume":"69","author":"S Boldo","year":"2019","unstructured":"Boldo, S., Faissole, F., Chapoutot, A.: Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Trans. Comput. 69, 1745\u20131756 (2019)","journal-title":"IEEE Trans. Comput."},{"key":"9686_CR15","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.-C.: Formal verification of floating-point programs. In: Kornerup, P., Muller, J.-M. (eds.) Proceedings of the 18th IEEE Symposium on Computer Arithmetic, pp. 187\u2013194, Montpellier, France (June 2007)","DOI":"10.1109\/ARITH.2007.20"},{"key":"9686_CR16","doi-asserted-by":"crossref","unstructured":"Boldo, S., Joldes, M., Muller, J.-M., Popescu, V.: Formal verification of a floating-point expansion renormalization algorithm. In: Proceedings of the 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, September (2017)","DOI":"10.1007\/978-3-319-66107-0_7"},{"issue":"1","key":"9686_CR17","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"9686_CR18","first-page":"243","volume-title":"20th IEEE Symposium on Computer Arithmetic","author":"S Boldo","year":"2011","unstructured":"Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) 20th IEEE Symposium on Computer Arithmetic, pp. 243\u2013252. T\u00fcbingen, Germany (2011)"},{"key":"9686_CR19","volume-title":"Computer Arithmetic and Formal Proofs","author":"S Boldo","year":"2017","unstructured":"Boldo, S., Melquiond, G.: Computer Arithmetic and Formal Proofs. ISTE Press - Elsevier, London (2017)"},{"key":"9686_CR20","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Chapoutot, A., Djoudi, A.: Enclosing temporal evolution of dynamical systems using numerical methods. In: NASA Formal Methods, volume 7871 in Lecture Notes in Computer Science, pp. 108\u2013123. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_8"},{"key":"9686_CR21","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Martel, M.: GRKLib: a guaranteed Runge-Kutta library. In: Computer Arithmetic and Validated Numerics. IEEE, In International Symposium on Scientific Computing (2006)","DOI":"10.1109\/SCAN.2006.20"},{"key":"9686_CR22","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1086\/105423","volume":"46","author":"D Brouwer","year":"1937","unstructured":"Brouwer, D.: On the accumulation of errors in numerical integration. Astron. J. 46, 149\u2013153 (1937)","journal-title":"Astron. J."},{"issue":"1\u20132","key":"9686_CR23","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0377-0427(93)90275-G","volume":"45","author":"JC Butcher","year":"1993","unstructured":"Butcher, J.C., Johnston, P.B.: Estimating local truncation errors for Runge-Kutta methods. J. Comput. Appl. Math. 45(1\u20132), 203\u2013212 (1993)","journal-title":"J. Comput. Appl. Math."},{"key":"9686_CR24","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first-order theory. PhD thesis, Ecole Polytechnique X (2012)"},{"issue":"1","key":"9686_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1644001.1644003","volume":"37","author":"M Daumas","year":"2010","unstructured":"Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. Trans. Math. Softw. 37(1), 1\u201320 (2010)","journal-title":"Trans. Math. Softw."},{"key":"9686_CR26","volume-title":"Analyse num\u00e9rique et \u00e9quations diff\u00e9rentielles","author":"J-P Demailly","year":"2016","unstructured":"Demailly, J.-P.: Analyse num\u00e9rique et \u00e9quations diff\u00e9rentielles. Collection Grenoble sciences, Les Ulis - EDP Sciences (2016)"},{"key":"9686_CR27","doi-asserted-by":"crossref","unstructured":"Ding, Z.: Solving Bateman equation for xenon transient analysis using numerical methods. In: MATEC Web of Conferences, vol. 186, p. 01004. EDP Sciences (2018)","DOI":"10.1051\/matecconf\/201818601004"},{"key":"9686_CR28","unstructured":"dit Sandretto, J.A., Chapoutot, A.: Validated explicit and implicit Runge-Kutta methods. Reliab. Comput. 22: 79 (2016)"},{"key":"9686_CR29","unstructured":"Euler, L.: Institutionum calculi integralis, 3 vols. Petropoli: Impensis Academia Imperialis Scientiarum. In: Euler, OO, Series 1, pp. 11\u201313 (1768)"},{"key":"9686_CR30","unstructured":"Fousse, L.: Int\u00e9gration num\u00e9rique avec erreur born\u00e9e en pr\u00e9cision arbitraire. PhD thesis (2006)"},{"key":"9686_CR31","doi-asserted-by":"crossref","unstructured":"Fousse, L.: Accurate multiple-precision Gauss\u2013Legendre quadrature. In: 18th IEEE Symposium on Computer Arithmetic, pp. 150\u2013160. IEEE Computer Society (2007)","DOI":"10.1109\/ARITH.2007.8"},{"issue":"1","key":"9686_CR32","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1051\/ita:2007004","volume":"41","author":"L Fousse","year":"2007","unstructured":"Fousse, L.: Multiple-precision correctly rounded Newton-Cotes quadrature. Informatique Th\u00e9orique et Applications 41(1), 103\u2013121 (2007)","journal-title":"Informatique Th\u00e9orique et Applications"},{"issue":"2","key":"9686_CR33","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/1236463.1236468","volume":"33","author":"L Fousse","year":"2007","unstructured":"Fousse, L., Hanrot, G., Lef\u00e8vre, V., P\u00e9lissier, P., Zimmermann, P.: MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2), 13 (2007)","journal-title":"ACM Trans. Math. Softw."},{"issue":"1","key":"9686_CR34","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D Goldberg","year":"1991","unstructured":"Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23(1), 5\u201348 (1991)","journal-title":"ACM Comput. Surv."},{"key":"9686_CR35","volume-title":"Matrix Computations","author":"GH Golub","year":"1996","unstructured":"Golub, G.H., Van Loan, C.F.: Matrix Computations, 3rd edn. The Johns Hopkins University Press, Baltimore (1996)","edition":"3"},{"key":"9686_CR36","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Static analysis of finite precision computations. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 232\u2013247. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"9686_CR37","unstructured":"Gu\u00e9neau, A.: Procrastination, a proof engineering technique. Coq Workshop 2018 (April 2018)"},{"key":"9686_CR38","volume-title":"Elementary Applied Partial Differential Equations","author":"R Haberman","year":"1983","unstructured":"Haberman, R.: Elementary Applied Partial Differential Equations, vol. 987. Prentice Hall, Englewood Cliffs, NJ (1983)"},{"issue":"2","key":"9686_CR39","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s10543-008-0170-3","volume":"48","author":"E Hairer","year":"2008","unstructured":"Hairer, E., McLachlan, R.I., Razakarivony, A.: Achieving Brouwer\u2019s law with implicit Runge-Kutta methods. BIT Numer. Math. 48(2), 231\u2013243 (2008)","journal-title":"BIT Numer. Math."},{"key":"9686_CR40","volume-title":"Solving Ordinary Differential Equations I: Nonstiff Problems","author":"E Hairer","year":"1993","unstructured":"Hairer, E., Norsett, S.P., Wanner, G.: Solving Ordinary Differential Equations I: Nonstiff Problems, vol. 8. Springer, New York (1993)"},{"key":"9686_CR41","volume-title":"Error Propagation for Difference Methods","author":"P Henrici","year":"1963","unstructured":"Henrici, P.: Error Propagation for Difference Methods. Wiley, New York (1963)"},{"key":"9686_CR42","volume-title":"A Survey of Componentwise Perturbation Theory","author":"NJ Higham","year":"1994","unstructured":"Higham, N.J.: A Survey of Componentwise Perturbation Theory, vol. 48. American Mathematical Society, Providence (1994)"},{"key":"9686_CR43","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718027","volume-title":"Accuracy and Stability of Numerical Algorithms","author":"NJ Higham","year":"2002","unstructured":"Higham, N.J.: Accuracy and Stability of Numerical Algorithms, 2nd edn. Society for Industrial and Applied Mathematics, Philadelphia (2002)","edition":"2"},{"key":"9686_CR44","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717778","volume-title":"Functions of Matrices: Theory and Computation","author":"NJ Higham","year":"2008","unstructured":"Higham, N.J.: Functions of Matrices: Theory and Computation, vol. 104. Siam, Philadelphia (2008)"},{"key":"9686_CR45","first-page":"8","volume":"754\u20132008","author":"IEEE standard for floating-point arithmetic","year":"2008","unstructured":"IEEE standard for floating-point arithmetic: IEEE Std 754\u20132008, 8 (2008)","journal-title":"IEEE Std"},{"key":"9686_CR46","doi-asserted-by":"crossref","unstructured":"Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29\u2014May 1, 2014. Proceedings, volume 8430 of Lecture Notes in Computer Science, pp. 113\u2013127. Springer (2014)","DOI":"10.1007\/978-3-319-06200-6_9"},{"key":"9686_CR47","doi-asserted-by":"crossref","unstructured":"Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: NASA Formal Methods Symposium, pp. 113\u2013127. Springer (2014)","DOI":"10.1007\/978-3-319-06200-6_9"},{"issue":"1","key":"9686_CR48","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-017-9448-y","volume":"61","author":"F Immler","year":"2018","unstructured":"Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1), 73\u2013111 (2018)","journal-title":"J. Autom. Reason."},{"key":"9686_CR49","doi-asserted-by":"crossref","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A.P. (eds.) Third International Conference on Interactive Theorem Proving, ITP, volume 7406 of Lecture Notes in Computer Science, pp. 377\u2013392. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_26"},{"key":"9686_CR50","doi-asserted-by":"crossref","unstructured":"Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, C.J., Merz, S. (eds.) Proceedings of the 7th International Conference on Interactive Theorem Proving, pp. 184\u2013199, Nancy, France (March 2016). Springer","DOI":"10.1007\/978-3-319-43144-4_12"},{"key":"9686_CR51","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1090\/mcom\/3234","volume":"87","author":"C-P Jeannerod","year":"2016","unstructured":"Jeannerod, C.-P., Rump, S.M.: On relative errors of floating-point operations: optimal bounds and applications. Math. Comput. 87, 803\u2013819 (2016)","journal-title":"Math. Comput."},{"key":"9686_CR52","volume":"402","author":"S Kumar Das","year":"2018","unstructured":"Kumar Das, S., Roy, S.: Finite element analysis of aircraft wing using carbon fiber reinforced polymer and glass fiber reinforced polymer. J. Phys. Conf. Ser. 402, 012077 (2018)","journal-title":"J. Phys. Conf. Ser."},{"key":"9686_CR53","first-page":"435","volume":"46","author":"W Kutta","year":"1901","unstructured":"Kutta, W.: Beitrag zur naherungsweisen integration totaler differentialgleichungen. Z. Angew. Math. Phys. 46, 435\u2013453 (1901)","journal-title":"Z. Angew. Math. Phys."},{"key":"9686_CR54","doi-asserted-by":"crossref","unstructured":"Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally verified approximations of definite integrals. In: Blanchette, J.C., Merz, S. (eds.) Proceedings of the 7th Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, pp. 274\u2013289, Nancy, France, (August 2016)","DOI":"10.1007\/978-3-319-43144-4_17"},{"issue":"2","key":"9686_CR55","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10817-018-9463-7","volume":"62","author":"A Mahboubi","year":"2019","unstructured":"Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally verified approximations of definite integrals. J. Autom. Reason. 62(2), 281\u2013300 (2019)","journal-title":"J. Autom. Reason."},{"key":"9686_CR56","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components (2017)"},{"key":"9686_CR57","unstructured":"Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) International Joint Conference on Automated Reasoning, IJCAR 2008, volume 5195 of Lecture Notes in Artifical Intelligence, pp. 2\u201317, Sydney, Australia (August 2008). Springer"},{"issue":"4","key":"9686_CR58","first-page":"801","volume":"20","author":"C Moler","year":"1978","unstructured":"Moler, C., Van Loan, C.F.: Nineteen dubious ways to compute the exponential of a matrix. Soc. Indust. Appl. Math. Rev. 20(4), 801\u2013836 (1978)","journal-title":"Soc. Indust. Appl. Math. Rev."},{"key":"9686_CR59","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"J-M Muller","year":"2010","unstructured":"Muller, J.-M., Brisebarre, N., de Dinechin, F., Jeannerod, C.-P., Lef\u00e8vre, V., Melquiond, G., Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user, Nathalie Revol (2010)"},{"key":"9686_CR60","doi-asserted-by":"crossref","unstructured":"Orogat, A., Liu, I., El-Roby, A.: Cbench: Towards better evaluation of question answering over knowledge graphs. arXiv preprint arXiv:2105.00811 (2021)","DOI":"10.14778\/3457390.3457398"},{"key":"9686_CR61","unstructured":"Pa\u015fca, I.: A formal verification for Kantorovitch\u2019s Theorem. In: Journ\u00e9es Francophones des Langages Applicatifs (January 2008)"},{"key":"9686_CR62","unstructured":"Pa\u015fca, I.: Formal proofs for theoretical properties of Newton\u2019s method (2010). INRIA Research Report RR-7228"},{"key":"9686_CR63","unstructured":"Pa\u015fca, I.: formal verification for numerical methods. PhD thesis, 11 (2010)"},{"key":"9686_CR64","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: Logic in Computer Science, pp. 541\u2013550. IEEE (2012)","DOI":"10.1109\/LICS.2012.64"},{"issue":"4","key":"9686_CR65","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00692009","volume":"58","author":"GD Quinlan","year":"1994","unstructured":"Quinlan, G.D.: Round-off error in long-term orbital integrations using multistep methods. Celest. Mech. Dyn. Astron. 58(4), 339\u2013351 (1994)","journal-title":"Celest. Mech. Dyn. Astron."},{"key":"9686_CR66","volume-title":"Difference Methods for Initial-Value Problems","author":"RD Richtmyer","year":"1967","unstructured":"Richtmyer, R.D., Keith, W.: Difference Methods for Initial-Value Problems. Interscience Publishers, Morton (1967)"},{"key":"9686_CR67","doi-asserted-by":"crossref","unstructured":"Rouhling, D.: A formal proof in Coq of a control function for the inverted pendulum. In: CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 1\u201314, Los Angeles, United States (January 2018)","DOI":"10.1145\/3176245.3167101"},{"issue":"2","key":"9686_CR68","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10817-015-9339-z","volume":"57","author":"P Roux","year":"2016","unstructured":"Roux, P.: Formal proofs of rounding error bounds\u2013with application to an automatic positive definiteness check. J. Autom. Reason. 57(2), 135\u2013156 (2016)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9686_CR69","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10543-015-0555-z","volume":"56","author":"SM Rump","year":"2016","unstructured":"Rump, S.M., B\u00fcnger, F., Jeannerod, C.-P.: Improved error bounds for floating-point products and Horner\u2019s scheme. BIT Numer. Math. 56(1), 293\u2013307 (2016)","journal-title":"BIT Numer. Math."},{"issue":"2","key":"9686_CR70","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01446807","volume":"46","author":"C Runge","year":"1895","unstructured":"Runge, C.: \u00dcber die numerische aufl\u00f6sung von differentialgleichungen. Math. Ann. 46(2), 167\u2013178 (1895)","journal-title":"Math. Ann."},{"issue":"1","key":"9686_CR71","first-page":"1","volume":"1","author":"G Scholz","year":"2014","unstructured":"Scholz, G., Scholz, F.: First-order differential equations in chemistry. ChemTexts 1(1), 1 (2014)","journal-title":"First-order differential equations in chemistry. ChemTexts"},{"key":"9686_CR72","unstructured":"Sibut\u00a0Pinote, T.: Investigations in computer-aided mathematics: experimentation, computation, and certification. PhD thesis (2017)"},{"key":"9686_CR73","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.trpro.2017.12.182","volume":"28","author":"I Smojver","year":"2017","unstructured":"Smojver, I., Ivan\u010devi\u0107, D.: Application of numerical methods in the improvement of safety of aeronautical structures. Transp. Res. Procedia 28, 164\u2013172 (2017)","journal-title":"Transp. Res. Procedia"},{"key":"9686_CR74","unstructured":"Tatum, J.B.: Physics Topics: Electricity and Magnetism, 2007, chapter 3. Free Online Textbook"},{"issue":"1\u20132","key":"9686_CR75","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0045-7825(98)80008-X","volume":"158","author":"CA Taylor","year":"1998","unstructured":"Taylor, C.A., Hughes, T.J.R., Zarins, C.K.: Finite element modeling of blood flow in arteries. Comput. Methods Appl. Mech. Eng. 158(1\u20132), 155\u2013196 (1998)","journal-title":"Comput. Methods Appl. Mech. Eng."},{"key":"9686_CR76","doi-asserted-by":"crossref","unstructured":"Tekriwal, M., Duraisamy, K., Jeannin, J.-B.: A formal proof of the Lax equivalence theorem for finite difference schemes. In: NASA Formal Methods Symposium, pp. 322\u2013339. Springer (2021)","DOI":"10.1007\/978-3-030-76384-8_20"},{"issue":"1","key":"9686_CR77","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s002080010018","volume":"2","author":"W Tucker","year":"2002","unstructured":"Tucker, W.: A rigorous ODE solver and Smale\u2019s 14th problem. Found. Comput. Math. 2(1), 53\u2013117 (2002)","journal-title":"Found. Comput. Math."},{"key":"9686_CR78","unstructured":"US Government Accountability Office. Defense Patriot Missile: Software problem led to system failure at Dhahran, Saudi Arabia. US Government Accountability Office Reports, rapport no. GAO\/IMTEC-92-26 (1992)"},{"key":"9686_CR79","volume-title":"Solving ordinary differential Equations II","author":"G Wanner","year":"1996","unstructured":"Wanner, G., Hairer, E.: Solving ordinary differential Equations II. Springer, Berlin (1996)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09686-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09686-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09686-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T13:13:45Z","timestamp":1710767625000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09686-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,6]]},"references-count":79,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["9686"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09686-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,6]]},"assertion":[{"value":"13 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 October 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 December 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"1"}}