{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:32:50Z","timestamp":1743107570631,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030763831"},{"type":"electronic","value":"9783030763848"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-76384-8_20","type":"book-chapter","created":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:50:53Z","timestamp":1621381853000},"page":"322-339","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes"],"prefix":"10.1007","author":[{"given":"Mohit","family":"Tekriwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karthik","family":"Duraisamy","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":[[2021,5,19]]},"reference":[{"key":"20_CR1","unstructured":"Navier-stokes equations. https:\/\/www.grc.nasa.gov\/WWW\/k-12\/airplane\/nseqs.html. Accessed 20 Sep 2020"},{"key":"20_CR2","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: Elfic Coq library for formalization of Lax-Milgram theorem. https:\/\/www.lri.fr\/sboldo\/elfic\/index.html. Accessed 20 Sep 2020"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax-Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 79\u201389. ACM (2017)","DOI":"10.1145\/3018610.3018625"},{"key":"20_CR4","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":"20_CR5","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. Reasoning 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"20_CR6","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":"20_CR7","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Hierarchy Coq library. http:\/\/coquelicot.saclay.inria.fr\/html\/Coquelicot.Hierarchy.html. Accessed 20 Sep 2020"},{"issue":"1","key":"20_CR8","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":"20_CR9","unstructured":"Br\u00e9hard, F., Mahboubi, A., Pous, D.: A certificate-based approach to formally verified approximations. In: ITP 2019-Tenth International Conference on Interactive Theorem Proving, pp. 1\u201319 (2019)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-28891-3_9","volume-title":"NASA Formal Methods","author":"N Brisebarre","year":"2012","unstructured":"Brisebarre, N., et al.: Rigorous polynomial approximation using taylor models in Coq. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 85\u201399. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_9"},{"key":"20_CR11","unstructured":"Br\u00e9hard, F.: Numerical computation certified in functional spaces: A trilogue between rigorous polynomial approximations, symbolic computation and formal proof. Ph.D. thesis (2019)"},{"key":"20_CR12","unstructured":"Cohen, C.: Formalizing real analysis for polynomials (2010)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-66107-0_10","volume-title":"Interactive Theorem Proving","author":"C Cohen","year":"2017","unstructured":"Cohen, C., Rouhling, D.: A formal proof in Coq of lasalle\u2019s invariance principle. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 148\u2013163. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_10"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7","volume-title":"Software Engineering and Formal Methods","year":"2012","unstructured":"Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.): SEFM 2012. LNCS, vol. 7504. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7"},{"key":"20_CR15","unstructured":"Faissole, F.: Library on lax-milgram theorem (coqlm). https:\/\/www.lri.fr\/faissole\/these_coq.html. Accessed 30 Dec 2019"},{"key":"20_CR16","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"},{"issue":"7","key":"20_CR17","doi-asserted-by":"publisher","first-page":"1511","DOI":"10.1088\/0305-4470\/29\/7\/020","volume":"29","author":"G Hu","year":"1996","unstructured":"Hu, G., O\u2019Connell, R.F.: Analytical inversion of symmetric tridiagonal matrices. J. Phys. A Math. Gen. 29(7), 1511 (1996)","journal-title":"J. Phys. A Math. Gen."},{"key":"20_CR18","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":"20_CR19","unstructured":"Immler, F.: A Verified ODE Solver and Smale\u2019s 14th Problem. Dissertation, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen (2018)"},{"key":"20_CR20","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":"20_CR21","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":"20_CR22","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. Reasoning 62(2), 215\u2013236 (2019)","journal-title":"J. Autom. Reasoning"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Kirk, D.B., Mei, W., Hwu, W.: Chapter 10 - parallel patterns: sparse matrix-vector multiplication: an introduction to compaction and regularization in parallel algorithms. In: Kirk, D.B., Mei, W., Hwu, W. (eds.) Programming Massively Parallel Processors (Second Edition), pp. 217\u2013234. Morgan Kaufmann, Boston, second edition edn. (2013). https:\/\/doi.org\/10.1016\/B978-0-12-415992-1.00010-9, http:\/\/www.sciencedirect.com\/science\/article\/pii\/B9780124159921000109","DOI":"10.1016\/B978-0-12-415992-1.00010-9"},{"key":"20_CR24","unstructured":"Kreyszig, E.: Introductory Functional Analysis with Applications, vol. 1. Wiley, New York (1978)"},{"issue":"2","key":"20_CR25","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1002\/cpa.3160090206","volume":"9","author":"PD Lax","year":"1956","unstructured":"Lax, P.D., Richtmyer, R.D.: Survey of the stability of linear finite difference equations. Commun. Pure Appl. Math. 9(2), 267\u2013293 (1956)","journal-title":"Commun. Pure Appl. Math."},{"key":"20_CR26","unstructured":"Lelay, C.: How to express convergence for analysis in coq (2015)"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Martin-Dorel, \u00c9., Rideau, L., Th\u00e9ry, L., Mayero, M., Pasca, I.: Certified, efficient and sharp univariate taylor models in coq. In: 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 193\u2013200. IEEE (2013)","DOI":"10.1109\/SYNASC.2013.33"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-45685-6_17","volume-title":"Theorem Proving in Higher Order Logics","author":"M Mayero","year":"2002","unstructured":"Mayero, M.: Using theorem proving for numerical analysis correctness proof of an automatic differentiation algorithm. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 246\u2013262. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45685-6_17"},{"key":"20_CR29","unstructured":"Melquiond, G., \u00c9rik Martin-Dorel, M.M., Pasca, I., Rideau, L., Th\u00e9ry, L.: Interval Coq Library. http:\/\/coq-interval.gforge.inria.fr\/. Accessed 20 Sep 2020"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 246\u2013261. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_21"},{"key":"20_CR31","unstructured":"Pasca, I.: Formal Verification for Numerical Methods. Ph.D. thesis, Universit\u00e9 Nice Sophia Antipolis (2010)"},{"issue":"171","key":"20_CR32","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1090\/S0025-5718-1985-0790648-7","volume":"45","author":"J Sanz-Serna","year":"1985","unstructured":"Sanz-Serna, J., Palencia, C.: A general equivalence theorem in the theory of discretization methods. Math. Comput. 45(171), 143\u2013152 (1985)","journal-title":"Math. Comput."},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Tekriwal, M., Duraisamy, K., Jeannin, J.B.: A formal proof of the Lax equivalence theorem for finite difference schemes. arXiv preprint arXiv:2103.13534, https:\/\/arxiv.org\/abs\/2103.13534 (2021)","DOI":"10.1007\/978-3-030-76384-8_20"}],"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-030-76384-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T21:13:47Z","timestamp":1672175627000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-76384-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030763831","9783030763848"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-76384-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 May 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2021\/","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":"66","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":"21","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":"3","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":"32% - 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":"5","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}