{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:16Z","timestamp":1776423796793,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031606977","type":"print"},{"value":"9783031606984","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_3","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"37-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of\u00a0Asymptotic Convergence for\u00a0Stationary Iterative Methods"],"prefix":"10.1007","author":[{"given":"Mohit","family":"Tekriwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1137\/1037008","volume":"37","author":"R Bagnara","year":"1995","unstructured":"Bagnara, R.: A unified proof for the convergence of Jacobi and Gauss-Seidel methods. SIAM Rev. 37(1), 93\u201397 (1995)","journal-title":"SIAM Rev."},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14052-5_12","volume-title":"Interactive Theorem Proving","author":"S Boldo","year":"2010","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.) ITP 2010. LNCS, vol. 6172, pp. 147\u2013162. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_12"},{"issue":"4","key":"3_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. J. Autom. Reason. 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"3_CR4","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."},{"issue":"1","key":"3_CR5","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":"3_CR6","unstructured":"Cano, G., D\u00e9n\u00e8s, M.: Matrices \u00e0 blocs et en forme canonique. In: JFLA \u2013 Journ\u00e9es francophones des langages applicatifs (2013). https:\/\/hal.inria.fr\/hal-00779376"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Construction of real algebraic numbers in Coq. In: Interactive Theorem Proving (2012). https:\/\/hal.inria.fr\/hal-00671809","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-031-16681-5_2","volume-title":"Intelligent Computer Mathematics","author":"E Deniz","year":"2022","unstructured":"Deniz, E., Rashid, A., Hasan, O., Tahar, S.: On the formalization of the heat conduction problem in HOL. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 21\u201337. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_2"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"3_CR10","unstructured":"Hindmarsh, A.C.: Odepack, a systematized collection of ode solvers. Sci. Comput. 55\u201364 (1983)"},{"issue":"3","key":"3_CR11","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1145\/1089014.1089020","volume":"31","author":"AC Hindmarsh","year":"2005","unstructured":"Hindmarsh, A.C., et al.: SUNDIALS: suite of nonlinear and differential\/algebraic equation solvers. ACM Trans. Math. Softw. (TOMS) 31(3), 363\u2013396 (2005)","journal-title":"ACM Trans. Math. Softw. (TOMS)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-06200-6_9","volume-title":"NASA Formal Methods","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. LNCS, vol. 8430, pp. 113\u2013127. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_9"},{"key":"3_CR13","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":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-43144-4_12","volume-title":"Interactive Theorem Proving","author":"F Immler","year":"2016","unstructured":"Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 184\u2013199. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_12"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10817-018-9449-5","volume":"62","author":"F Immler","year":"2019","unstructured":"Immler, F., Traut, C.: The flow of ODEs: formalization of variational equation and Poincar\u00e9 map. J. Autom. Reason. 62(2), 215\u2013236 (2019)","journal-title":"J. Autom. Reason."},{"key":"3_CR16","unstructured":"Lancaster, P., Tismenetsky, M.: The Theory of Matrices: With Applications. Elsevier (1985)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Mahboubi, A., Cohen, C.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods Comput. Sci. 8 (2012)","DOI":"10.2168\/LMCS-8(1:2)2012"},{"key":"3_CR18","unstructured":"Pasca, I.: Formal verification for numerical methods. Ph.D. thesis, Universit\u00e9 Nice Sophia Antipolis (2010)"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"121","DOI":"10.2514\/3.20077","volume":"9","author":"JE Prussing","year":"1986","unstructured":"Prussing, J.E.: The principal minor test for semidefinite matrices. J. Guid. Control. Dyn. 9(1), 121\u2013122 (1986)","journal-title":"J. Guid. Control. Dyn."},{"issue":"3","key":"3_CR20","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1214\/aoms\/1177729998","volume":"20","author":"E Reich","year":"1949","unstructured":"Reich, E.: On the convergence of the classical iterative method of solving linear simultaneous equations. Ann. Math. Stat. 20(3), 448\u2013451 (1949)","journal-title":"Ann. Math. Stat."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Saad, Y.: Iterative Methods for Sparse Linear Systems, 2nd edn. Society for Industrial and Applied Mathematics (SIAM), Philadelphia (2003)","DOI":"10.1137\/1.9780898718003"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-031-42753-4_14","volume-title":"Intelligent Computer Mathematics","author":"M Tekriwal","year":"2023","unstructured":"Tekriwal, M., Appel, A.W., Kellison, A.E., Bindel, D., Jeannin, J.B.: Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method. In: Dubois, C., Kerber, M. (eds.) CICM 2023. LNCS, vol. 14101, pp. 206\u2013221. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-42753-4_14"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-030-76384-8_20","volume-title":"NASA Formal Methods","author":"M Tekriwal","year":"2021","unstructured":"Tekriwal, M., Duraisamy, K., Jeannin, J.-B.: A formal proof of the lax equivalence theorem for finite difference schemes. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 322\u2013339. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_20"},{"key":"3_CR24","unstructured":"Tekriwal, M., Miller, J., Jeannin, J.B.: Formalization of asymptotic convergence for stationary iterative methods (extended version) (2022). https:\/\/arxiv.org\/abs\/2202.05587"},{"key":"3_CR25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100699","volume":"123","author":"R Thiemann","year":"2021","unstructured":"Thiemann, R.: A Perron-Frobenius theorem for deciding matrix growth. J. Logical Algebraic Methods Program. 123, 100699 (2021)","journal-title":"J. Logical Algebraic Methods Program."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:02:37Z","timestamp":1716768157000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}