{"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":1776423798287,"version":"3.51.2"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,1,22]],"date-time":"2018-01-22T00:00:00Z","timestamp":1516579200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 1480"],"award-info":[{"award-number":["RTG 1480"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9448-y","type":"journal-article","created":{"date-parts":[[2018,1,22]],"date-time":"2018-01-22T13:25:37Z","timestamp":1516627537000},"page":"73-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["A Verified ODE Solver and the Lorenz Attractor"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5468-1513","authenticated-orcid":false,"given":"Fabian","family":"Immler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,22]]},"reference":[{"key":"9448_CR1","volume-title":"Refinement Calculus: A Systematic Introduction","author":"RJ Back","year":"2012","unstructured":"Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (2012)"},{"key":"9448_CR2","doi-asserted-by":"crossref","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: International Conference on Certified Programs and Proofs, pp. 362\u2013377. Springer, New York (2011)","DOI":"10.1007\/978-3-642-25379-9_26"},{"issue":"4","key":"9448_CR3","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. Journal of Automated Reasoning 50(4), 423\u2013456 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9255-4","journal-title":"Journal of Automated Reasoning"},{"key":"9448_CR4","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-38088-4_8","volume-title":"NASA Formal Methods, LNCS","author":"O Bouissou","year":"2013","unstructured":"Bouissou, O., Chapoutot, A., Djoudi, A.: Enclosing temporal evolution of dynamical systems using numerical methods. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, LNCS, vol. 7871, pp. 108\u2013123. Springer, New York (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_8"},{"key":"9448_CR5","doi-asserted-by":"publisher","unstructured":"Brun, C., Dufourd, J.F., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Computational Geometry 45(8), 436\u2013457 (2012). https:\/\/doi.org\/10.1016\/j.comgeo.2010.06.006. (Geometric Constraints and Reasoning)","DOI":"10.1016\/j.comgeo.2010.06.006"},{"issue":"1\u20134","key":"9448_CR6","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1023\/B:NUMA.0000049462.70970.b6","volume":"37","author":"L Figueiredo de","year":"2004","unstructured":"de Figueiredo, L., Stolfi, J.: Affine arithmetic: concepts and applications. Numerical Algorithms 37(1\u20134), 147\u2013158 (2004)","journal-title":"Numerical Algorithms"},{"key":"9448_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-78929-1_16","volume-title":"Hybrid Systems: Computation and Control, LNCS","author":"A Girard","year":"2008","unstructured":"Girard, A., Le Guernic, C.: Zonotope\/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) Hybrid Systems: Computation and Control, LNCS, vol. 4981, pp. 215\u2013228. Springer, New York (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_16"},{"key":"9448_CR8","volume-title":"GNU MP 6.0 Multiple Precision Arithmetic Library","author":"T Granlund","year":"2015","unstructured":"Granlund, T., et al.: GNU MP 6.0 Multiple Precision Arithmetic Library. Samurai Media Limited, Hong Kong (2015)"},{"issue":"9","key":"9448_CR9","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/583852.581501","volume":"37","author":"B Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. ACM SIGPLAN Not. 37(9), 235\u2013246 (2002)","journal-title":"ACM SIGPLAN Not."},{"key":"9448_CR10","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Data Refinement in Isabelle\/HOL","author":"F Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data Refinement in Isabelle\/HOL, pp. 100\u2013115. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_10"},{"key":"9448_CR11","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: International Workshop on Types for Proofs and Programs, pp. 160\u2013174. Springer, New York (2006)","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"9448_CR12","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Lecture Notes in Computer Science, vol. 3603, pp. 114\u2013129 (2005)","DOI":"10.1007\/11541868_8"},{"key":"9448_CR13","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Reis, G.D. Th\u00e9ry L. (eds.) Programming Languages for Mechanized Mathematics Systems (ACM SIGSAM PLMMS\u201909), pp. 38\u201345 (2009)"},{"key":"9448_CR14","first-page":"279","volume-title":"ITP 2013","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, pp. 279\u2013294. Springer, New York (2013)"},{"key":"9448_CR15","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: International Conference on Certified Programs and Proofs, pp. 131\u2013146. Springer, New York (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"9448_CR16","unstructured":"Hupel, L.: Dictionary Construction. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Dict_Construction.html, Formal proof development"},{"key":"9448_CR17","unstructured":"Hupel, L., Nipkow, T.: A verified compiler from Isabelle\/HOL to CakeML. Springer LNCS (2018). https:\/\/lars.hupel.info\/pub\/isabelle-cakeml.pdf"},{"key":"9448_CR18","first-page":"113","volume-title":"NFM 2014","author":"F Immler","year":"2014","unstructured":"Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014, pp. 113\u2013127. Springer, New York (2014)"},{"key":"9448_CR19","doi-asserted-by":"crossref","unstructured":"Immler, F.: A verified algorithm for geometric zonotope\/hyperplane intersection. In: CPP 2015, pp. 129\u2013136. ACM (2015)","DOI":"10.1145\/2676724.2693164"},{"key":"9448_CR20","first-page":"221","volume-title":"ITP 2015","author":"F Immler","year":"2015","unstructured":"Immler, F.: A verified enclosure for the Lorenz attractor (rough diamond). In: Urban, C., Zhang, X. (eds.) ITP 2015, pp. 221\u2013226. Springer, Berlin (2015)"},{"key":"9448_CR21","first-page":"37","volume-title":"TACAS 2015","author":"F Immler","year":"2015","unstructured":"Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015, pp. 37\u201351. Springer, Berlin (2015)"},{"key":"9448_CR22","unstructured":"Immler, F.: Affine Arithmetic. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Affine_Arithmetic.shtml, Formal proof development"},{"key":"9448_CR23","unstructured":"Immler, F., H\u00f6lzl, J.: Ordinary Differential Equations. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Ordinary_Differential_Equations.shtml, Formal proof development"},{"key":"9448_CR24","doi-asserted-by":"crossref","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: International Conference on Interactive Theorem Proving, pp. 377\u2013392. Springer, New York (2012)","DOI":"10.1007\/978-3-642-32347-8_26"},{"key":"9448_CR25","doi-asserted-by":"publisher","unstructured":"Immler, F., Traut, C.: The flow of ODEs: Formalization of variational equation and Poincar\u00e9 map. J. Autom. Reason. (2018). https:\/\/doi.org\/10.1007\/s10817-018-9449-5","DOI":"10.1007\/s10817-018-9449-5"},{"key":"9448_CR26","first-page":"184","volume-title":"ITP 2016","author":"F Immler","year":"2016","unstructured":"Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, pp. 184\u2013199. Springer, Cham (2016)"},{"key":"9448_CR27","doi-asserted-by":"crossref","unstructured":"Knuth, D.: Axioms and Hulls. Springer, Berlin (1992). Number 606 in Lecture Notes in Computer Science","DOI":"10.1007\/3-540-55611-7"},{"key":"9448_CR28","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: ACM SIGPLAN Notices, vol.\u00a049, pp. 179\u2013191. ACM (2014)","DOI":"10.1145\/2535838.2535841"},{"key":"9448_CR29","unstructured":"Lammich, P.: Refinement for monadic programs. Archive of Formal Proofs (2012). http:\/\/afp.sf.net\/entries\/Refine_Monadic.shtml, Formal proof development"},{"key":"9448_CR30","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Automatic data refinement. In: International Conference on Interactive Theorem Proving, pp. 84\u201399. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39634-2_9"},{"issue":"2","key":"9448_CR31","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1175\/1520-0469(1963)020<0130:DNF>2.0.CO;2","volume":"20","author":"EN Lorenz","year":"1963","unstructured":"Lorenz, E.N.: Deterministic nonperiodic flow. J. Atmos. Sci. 20(2), 130\u2013141 (1963). https:\/\/doi.org\/10.1175\/1520-0469(1963)020%3c0130:DNF%3e2.0.CO;2","journal-title":"J. Atmos. Sci."},{"key":"9448_CR32","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-319-43144-4_17","volume-title":"Formally Verified Approximations of Definite Integrals","author":"A Mahboubi","year":"2016","unstructured":"Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally Verified Approximations of Definite Integrals, pp. 274\u2013289. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_17"},{"key":"9448_CR33","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-3-642-39634-2_34","volume-title":"Interactive Theorem Proving, LNCS","author":"E Makarov","year":"2013","unstructured":"Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, LNCS, vol. 7998, pp. 463\u2013468. Springer, Berlin (2013)"},{"issue":"3","key":"9448_CR34","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10817-015-9350-4","volume":"57","author":"E Martin-Dorel","year":"2016","unstructured":"Martin-Dorel, E., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 57(3), 187\u2013217 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9350-4","journal-title":"J. Autom. Reason."},{"key":"9448_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry, Lecture Notes in Computer Science","author":"L Meikle","year":"2006","unstructured":"Meikle, L., Fleuriot, J.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, pp. 1\u201318. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11615798_1"},{"issue":"11","key":"9448_CR36","doi-asserted-by":"crossref","first-page":"3393","DOI":"10.1090\/S0002-9939-99-04936-9","volume":"127","author":"C Morales","year":"1999","unstructured":"Morales, C., Pacifico, M., Pujals, E.: Singular hyperbolic systems. Proc. Am. Math. Soc. 127(11), 3393\u20133401 (1999)","journal-title":"Proc. Am. Math. Soc."},{"key":"9448_CR37","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Lester, D.: Real number calculations and theorem proving. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS, pp. 195\u2013210 (2005)","DOI":"10.1007\/11541868_13"},{"key":"9448_CR38","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Logical Environments, pp. 164\u2013188. Cambridge University Press (1993)"},{"key":"9448_CR39","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS. Springer, Heidelberg (2002)"},{"key":"9448_CR40","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science","author":"D Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 2152, pp. 346\u2013361. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/3-540-44755-5_24"},{"key":"9448_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0003-8","volume-title":"Dynamical Systems\u2014Stability, Symbolic Dynamics, and Chaos","author":"C Robinson","year":"1999","unstructured":"Robinson, C.: Dynamical Systems\u2014Stability, Symbolic Dynamics, and Chaos. CRC Press, Boca Raton (1999). https:\/\/doi.org\/10.1007\/978-1-4613-0003-8"},{"issue":"3","key":"9448_CR42","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1587\/nolta.6.341","volume":"6","author":"SM Rump","year":"2015","unstructured":"Rump, S.M., Kashiwagi, M.: Implementation and improvements of affine arithmetic. Nonlinear Theory Appl. IEICE 6(3), 341\u2013359 (2015). https:\/\/doi.org\/10.1587\/nolta.6.341","journal-title":"Nonlinear Theory Appl. IEICE"},{"issue":"2","key":"9448_CR43","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF03025291","volume":"20","author":"S Smale","year":"1998","unstructured":"Smale, S.: Mathematical problems for the next century. Math. Intell. 20(2), 7\u201315 (1998). https:\/\/doi.org\/10.1007\/BF03025291","journal-title":"Math. Intell."},{"key":"9448_CR44","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods Symposium, pp. 383\u2013397. Springer, New York (2013)","DOI":"10.1007\/978-3-642-38088-4_26"},{"key":"9448_CR45","doi-asserted-by":"publisher","unstructured":"Sparrow, C.: The Lorenz Equations: Bifurcations, Chaos, and Strange Attractors. No.\u00a041 in Applied Mathematical Sciences. Springer. New York. https:\/\/doi.org\/10.1007\/978-1-4612-5767-7","DOI":"10.1007\/978-1-4612-5767-7"},{"key":"9448_CR46","unstructured":"Tucker, W.: My thesis: The lorenz attractor exists. http:\/\/www2.math.uu.se\/~warwick\/main\/pre_thesis.html"},{"issue":"12","key":"9448_CR47","doi-asserted-by":"crossref","first-page":"1197","DOI":"10.1016\/S0764-4442(99)80439-X","volume":"328","author":"W Tucker","year":"1999","unstructured":"Tucker, W.: The Lorenz attractor exists. Comptes Rendus de l\u2019Acad\u00e9mie des Sciences-Series I-Mathematics 328(12), 1197\u20131202 (1999)","journal-title":"Comptes Rendus de l\u2019Acad\u00e9mie des Sciences-Series I-Mathematics"},{"issue":"1","key":"9448_CR48","doi-asserted-by":"crossref","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."},{"issue":"3","key":"9448_CR49","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/BF03025276","volume":"22","author":"M Viana","year":"2000","unstructured":"Viana, M.: What\u2019s new on Lorenz strange attractors? Math. Intell. 22(3), 6\u201319 (2000)","journal-title":"Math. Intell."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9448-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9448-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9448-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T13:29:06Z","timestamp":1570627746000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9448-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,22]]},"references-count":49,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9448"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9448-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,22]]}}}