{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:18Z","timestamp":1776423798044,"version":"3.51.2"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031212215","type":"print"},{"value":"9783031212222","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-21222-2_9","type":"book-chapter","created":{"date-parts":[[2022,12,15]],"date-time":"2022-12-15T09:04:55Z","timestamp":1671095095000},"page":"147-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Verified Numerical Methods for\u00a0Ordinary Differential Equations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3177-7958","authenticated-orcid":false,"given":"Ariel E.","family":"Kellison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,16]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1017\/S0962492902000144","volume":"12","author":"E Hairer","year":"2003","unstructured":"Hairer, E., Lubich, C., Wanner, G.: Geometric numerical integration illustrated by the St\u00f6rmer-Verlet method. Acta Numerica 12, 399\u2013450 (2003)","journal-title":"Acta Numerica"},{"issue":"1","key":"9_CR2","first-page":"21","volume":"105","author":"NS Nedialkov","year":"1999","unstructured":"Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comput. 105(1), 21\u201368 (1999)","journal-title":"Appl. Math. Comput."},{"issue":"10","key":"9_CR3","doi-asserted-by":"publisher","first-page":"1145","DOI":"10.1016\/j.apnum.2006.10.006","volume":"57","author":"Y Lin","year":"2007","unstructured":"Lin, Y., Stadtherr, M.A.: Validated solutions of initial value problems for parametric ODEs. Appl. Numer. Math. 57(10), 1145\u20131162 (2007)","journal-title":"Appl. Numer. Math."},{"key":"9_CR4","unstructured":"dit Sandretto, J.A., Chapoutot, A.: Validated explicit and implicit Runge-Kutta methods. Reliable Computing Electronic Edition, 22 July 2016"},{"issue":"4","key":"9_CR5","first-page":"370","volume":"15","author":"A Rauh","year":"2011","unstructured":"Rauh, A., Auer, E.: Verified simulation of ODEs and their solution. Reliab. Comput. 15(4), 370\u2013381 (2011)","journal-title":"Reliab. Comput."},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-57172-5_6","volume-title":"Advances in Software Tools for Scientific Computing","author":"NS Nedialkov","year":"2000","unstructured":"Nedialkov, N.S., Jackson, K.R.: ODE software that computes guaranteed bounds on the solution. In: Langtangen, H.P., Bruaset, A.M., Quak, E. (eds.) Advances in Software Tools for Scientific Computing, pp. 197\u2013224. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-57172-5_6"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), p. 4 (2006)","DOI":"10.1109\/SCAN.2006.28"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"issue":"1","key":"9_CR9","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":"9_CR10","volume-title":"Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System","author":"S Boldo","year":"2017","unstructured":"Boldo, S., Melquiond, G.: Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. Elsevier, Amsterdam (2017)"},{"key":"9_CR11","unstructured":"Appel, A.W., Kellison, A.E.: VCFloat2: floating-point error analysis in Coq. Draft (2022)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., Mountcastle, P., Meister, B., Lethin, R.: A unified Coq framework for verifying C programs with floating-point computations. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pp. 15\u201326. Association for Computing Machinery, New York (2016)","DOI":"10.1145\/2854065.2854066"},{"key":"9_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78862-1","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, 2nd rev. edition. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-3-540-78862-1. Corr. 3rd printing edition, 1993","edition":"2nd rev. editio"},{"key":"9_CR14","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717839","volume-title":"Finite Difference Methods for Ordinary and Partial Differential Equations","author":"RJ LeVeque","year":"2007","unstructured":"LeVeque, R.J.: Finite Difference Methods for Ordinary and Partial Differential Equations. Society for Industrial and Applied Mathematics, Philadelphia (2007)"},{"key":"9_CR15","series-title":"Springer Series in Computational Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-30666-8","volume-title":"Geometric Numerical Integration. Structure-Preserving Algorithms for Ordinary Differential Equations","author":"E Hairer","year":"2006","unstructured":"Hairer, E., Lubich, C., Wanner, G.: Geometric Numerical Integration. Structure-Preserving Algorithms for Ordinary Differential Equations. Springer Series in Computational Mathematics, vol. 31, 2nd edn. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/3-540-30666-8","edition":"2"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1017\/S0962492917000101","volume":"27","author":"N Bou-Rabee","year":"2018","unstructured":"Bou-Rabee, N., Sanz-Serna, J.M.: Geometric integrators and the Hamiltonian Monte Carlo method. Acta Numerica 27, 113\u2013206 (2018)","journal-title":"Acta Numerica"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"A1556","DOI":"10.1137\/130932740","volume":"36","author":"S Blanes","year":"2014","unstructured":"Blanes, S., Casas, F., Sanz-Serna, J.M.: Numerical integrators for the hybrid Monte Carlo method. SIAM J. Sci. Comput. 36(4), A1556\u2013A1580 (2014)","journal-title":"SIAM J. Sci. Comput."},{"key":"9_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03972-4_4","volume-title":"The Graduate Student\u2019s Guide to Numerical Analysis \u201998","author":"RD Skeel","year":"1999","unstructured":"Skeel, R.D.: Integration schemes for molecular dynamics and related applications. In: Ainsworth, M., Levesley, J., Marletta, M. (eds.) The Graduate Student\u2019s Guide to Numerical Analysis \u201998. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-662-03972-4_4"},{"key":"9_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/s10703-020-00353-1","volume":"58","author":"L Beringer","year":"2021","unstructured":"Beringer, L., Appel, A.W.: Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58, 322\u2013345 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00353-1","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"9_CR21","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/j.camwa.2014.06.004","volume":"68","author":"S Boldo","year":"2014","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Trusting computations: a mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3), 325\u2013352 (2014)","journal-title":"Comput. Math. Appl."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Boldo, S., Faissole, F., Chapoutot, A.: Round-off error analysis of explicit one-step numerical integration methods. In: 24th IEEE Symposium on Computer Arithmetic, London, UK, July 2017","DOI":"10.1109\/ARITH.2017.22"},{"issue":"1","key":"9_CR23","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. ACM Trans. Math. Softw. 37(1), 1\u201320 (2010)","journal-title":"ACM Trans. Math. Softw."},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F de Dinechin","year":"2011","unstructured":"de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242\u2013253 (2011)","journal-title":"IEEE Trans. Comput."},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-32347-8_26","volume-title":"Interactive Theorem Proving","author":"F Immler","year":"2012","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 377\u2013392. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_26"},{"key":"9_CR26","volume-title":"Guaranteed Error Bounds for Ordinary Differential Equations","author":"GF Corliss","year":"1994","unstructured":"Corliss, G.F.: Guaranteed Error Bounds for Ordinary Differential Equations. Oxford University Press, Oxford (1994)"},{"issue":"6","key":"9_CR27","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1023\/A:1014798618404","volume":"7","author":"NS Nedialkov","year":"2001","unstructured":"Nedialkov, N.S., Jackson, K.R., Pryce, J.D.: An effective high-order interval method for validating existence and uniqueness of the solution of an IVP for an ODE. Reliab. Comput. 7(6), 449\u2013465 (2001)","journal-title":"Reliab. Comput."},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/S0168-9274(01)00155-6","volume":"42","author":"KR Jackson","year":"2002","unstructured":"Jackson, K.R., Nedialkov, N.S.: Some recent advances in validated methods for IVPs for ODEs. Appl. Numer. Math. 42(1), 269\u2013284 (2002)","journal-title":"Appl. Numer. Math."},{"key":"9_CR29","unstructured":"Rihm, R.: Interval methods for initial value problems in ODEs. In: Topics in Validated Computations: Proceedings of IMACS-GAMM International Workshop on Validated Computation, September 1993"},{"issue":"1","key":"9_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10915-004-4629-3","volume":"25","author":"LF Shampine","year":"2005","unstructured":"Shampine, L.F.: Error estimation and control for ODEs. J. Sci. Comput. 25(1), 3\u201316 (2005)","journal-title":"J. Sci. Comput."},{"issue":"2","key":"9_CR31","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1137\/S1064827503420969","volume":"26","author":"Y Cao","year":"2004","unstructured":"Cao, Y., Petzold, L.: A posteriori error estimation and global error control for ordinary differential equations by the adjoint method. SIAM J. Sci. Comput. 26(2), 359\u2013374 (2004)","journal-title":"SIAM J. Sci. Comput."},{"issue":"1","key":"9_CR32","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s11075-016-0250-4","volume":"76","author":"B Kehlet","year":"2017","unstructured":"Kehlet, B., Logg, A.: A posteriori error analysis of round-off errors in the numerical solution of ordinary differential equations. Numer. Algorithms 76(1), 191\u2013210 (2017)","journal-title":"Numer. Algorithms"}],"container-title":["Lecture Notes in Computer Science","Software Verification and Formal Methods for ML-Enabled Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-21222-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,10]],"date-time":"2024-10-10T13:10:43Z","timestamp":1728565843000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21222-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212215","9783031212222"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21222-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"16 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NSV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Numerical Software Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nsv2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nsv22.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}