{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:49Z","timestamp":1767928009664,"version":"3.49.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,8,14]],"date-time":"2012-08-14T00:00:00Z","timestamp":1344902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10817-012-9255-4","type":"journal-article","created":{"date-parts":[[2012,8,13]],"date-time":"2012-08-13T14:48:39Z","timestamp":1344869319000},"page":"423-456","source":"Crossref","is-referenced-by-count":54,"title":["Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program"],"prefix":"10.1007","volume":"50","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Cl\u00e9ment","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Weis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,14]]},"reference":[{"key":"9255_CR1","unstructured":"Achenbach, J.D.: Wave Propagation in Elastic Solids. North Holland, Amsterdam (1973)"},{"key":"9255_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107325937","volume-title":"Special Functions","author":"GE Andrews","year":"1999","unstructured":"Andrews, G.E., Askey, R., Roy, R.: Special Functions. Cambridge University Press, Cambridge (1999)"},{"key":"9255_CR3","doi-asserted-by":"crossref","first-page":"327","DOI":"10.2307\/2978081","volume":"79","author":"R Askey","year":"1972","unstructured":"Askey, R., Gasper, G.: Certain rational functions whose power series have positive coefficients. Am. Math. Mon. 79, 327\u2013341 (1972)","journal-title":"Am. Math. Mon."},{"issue":"4","key":"9255_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s10817-007-9066-1","volume":"38","author":"J Avigad","year":"2007","unstructured":"Avigad, J., Donnelly, K.: A decision procedure for linear \u201cBig O\u201d equations. J. Autom. Reason. 38(4), 353\u2013373 (2007)","journal-title":"J. Autom. Reason."},{"key":"9255_CR5","first-page":"298","volume-title":"19th International Conference on Computer Aided Verification (CAV \u201907), LNCS, vol. 4590","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: 19th International Conference on Computer Aided Verification (CAV \u201907), LNCS, vol. 4590, pp. 298\u2013302. Springer, Berlin (2007)"},{"key":"9255_CR6","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language, version 1.5 (2009). URL http:\/\/frama-c.cea.fr\/acsl.html"},{"key":"9255_CR7","unstructured":"B\u00e9cache, E.: \u00c9tude de sch\u00e9mas num\u00e9riques pour la r\u00e9solution de l\u2019\u00e9quation des ondes. Master Mod\u00e9lisation et simulation, Cours ENSTA (2009). URL http:\/\/www-rocq.inria.fr\/~becache\/COURS-ONDES\/Poly-num-0209.pdf"},{"key":"9255_CR8","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9255_CR9","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201908), LNCS, vol. 5170","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201908), LNCS, vol. 5170, pp. 86\u2013101. Springer, Montreal (2008)"},{"key":"9255_CR10","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008). URL http:\/\/alt-ergo.lri.fr\/"},{"key":"9255_CR11","unstructured":"Boldo, S.: Preuves formelles en arithm\u00e9tiques \u00e0 virgule flottante. Ph.D. thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon (2004)"},{"key":"9255_CR12","first-page":"91","volume-title":"36th International Colloquium on Automata, Languages and Programming, LNCS - ARCoSS, vol. 5556","author":"S Boldo","year":"2009","unstructured":"Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming, LNCS - ARCoSS, vol. 5556, pp. 91\u2013102. Springer, Rhodos (2009)"},{"key":"9255_CR13","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1109\/ARITH.2007.20","volume-title":"18th IEEE International Symposium on Computer Arithmetic","author":"S Boldo","year":"2007","unstructured":"Boldo, S., Filli\u00e2tre, J.C.: Formal verification of floating-point programs. In: 18th IEEE International Symposium on Computer Arithmetic, pp. 187\u2013194. Montpellier, France (2007)"},{"issue":"2","key":"9255_CR14","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s11334-011-0151-6","volume":"7","author":"S Boldo","year":"2011","unstructured":"Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innovations Syst. Softw. Eng. 7(2), 151\u2013160 (2011)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"9255_CR15","first-page":"59","volume-title":"16th Calculemus Symposium, Lecture Notes in Artificial Intelligence, vol. 5625","author":"S Boldo","year":"2009","unstructured":"Boldo, S., Filli\u00e2tre, J.C., Melquiond, G.: Combining Coq and Gappa for certifying floating-point programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) 16th Calculemus Symposium, Lecture Notes in Artificial Intelligence, vol. 5625, pp. 59\u201374. Grand Bend, ON, Canada (2009)"},{"key":"9255_CR16","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-642-14052-5_12","volume-title":"1st Interactive Theorem Proving Conference (ITP), LNCS, vol. 6172","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.) 1st Interactive Theorem Proving Conference (ITP), LNCS, vol. 6172, pp. 147\u2013162. Springer, Edinburgh (2010)"},{"key":"9255_CR17","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":"9255_CR18","doi-asserted-by":"crossref","unstructured":"Brekhovskikh, L.M., Goncharov, V.: Mechanics of Continua and Wave Dynamics. Springer (1994)","DOI":"10.1007\/978-3-642-85034-9"},{"key":"9255_CR19","doi-asserted-by":"crossref","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): semantical combination of congruence closure with solvable theories. In: Post-Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Electronic Notes in Computer Science, vol. 198-2, pp. 51\u201369. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.080"},{"key":"9255_CR20","doi-asserted-by":"crossref","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) Colog\u201988, LNCS, vol. 417. Springer (1990)","DOI":"10.1007\/3-540-52335-9_47"},{"issue":"2","key":"9255_CR21","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1147\/rd.112.0215","volume":"11","author":"R Courant","year":"1967","unstructured":"Courant, R., Friedrichs, K., Lewy, H.: On the partial difference equations of mathematical physics. IBM J. Res. Develop. 11(2), 215\u2013234 (1967)","journal-title":"IBM J. Res. Develop."},{"key":"9255_CR22","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyzer. In: ESOP, no. 3444 in LNCS, pp. 21\u201330 (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"9255_CR23","volume-title":"2nd International Workshop on Types for Proofs and Programs (TYPES 2002), LNCS, vol. 2646","author":"L Cruz-Filipe","year":"2002","unstructured":"Cruz-Filipe, L.: A constructive formalization of the fundamental theorem of calculus. In: Geuvers, H., Wiedijk, F. (eds.) 2nd International Workshop on Types for Proofs and Programs (TYPES 2002), LNCS, vol. 2646. Springer, Berg en Dal (2002)"},{"issue":"1","key":"9255_CR24","doi-asserted-by":"crossref","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":"9255_CR25","doi-asserted-by":"crossref","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library for floating-point numbers and its application to exact computing. In: TPHOLs, pp. 169\u2013184 (2001)","DOI":"10.1007\/3-540-44755-5_13"},{"key":"9255_CR26","doi-asserted-by":"crossref","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: FMICS, LNCS, vol. 5825, pp. 53\u201369. Springer (2009)","DOI":"10.1007\/978-3-642-04570-7_6"},{"issue":"2","key":"9255_CR27","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F Dinechin de","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":"9255_CR28","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3, an efficient SMT solver. In: TACAS, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9255_CR29","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), LNCS, vol. 1125","author":"B Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS. In: von Wright, J., Grundy, J., Harrison, J. (eds.) 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201996), LNCS, vol. 1125, pp. 141\u2013156. Springer, Turku (1996)"},{"key":"9255_CR30","first-page":"173","volume-title":"19th International Conference on Computer Aided Verification, LNCS, vol. 4590","author":"JC Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: 19th International Conference on Computer Aided Verification, LNCS, vol. 4590, pp. 173\u2013177. Springer, Berlin (2007)"},{"key":"9255_CR31","doi-asserted-by":"crossref","unstructured":"Fleuriot, J.D.: On the mechanization of real analysis in Isabelle\/HOL. In: Aagaard, M., Harrison, J. (eds.) 13th International Conference on Theorem Proving and Higher-Order Logic (TPHOLs\u201900), LNCS, vol. 1869, pp. 145\u2013161. Springer (2000)","DOI":"10.1007\/3-540-44659-1_10"},{"issue":"4","key":"9255_CR32","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R Gamboa","year":"2001","unstructured":"Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason. 27(4), 323\u2013351 (2001)","journal-title":"J. Autom. Reason."},{"key":"9255_CR33","first-page":"79","volume-title":"1st International Workshop on Types for Proofs and Programs (TYPES 2000), LNCS, vol. 2277","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Niqui, M.: Constructive reals in Coq: axioms and categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) 1st International Workshop on Types for Proofs and Programs (TYPES 2000), LNCS, vol. 2277, pp. 79\u201395. Springer, Durham (2002)"},{"key":"9255_CR34","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"9255_CR35","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T.F. (eds.) 18th International Conference on Theorem Proving and Higher-Order Logic (TPHOLs\u201905), LNCS, vol. 3603, pp. 114\u2013129. Springer (2005)","DOI":"10.1007\/11541868_8"},{"key":"9255_CR36","unstructured":"John, F.: Partial Differential Equations. Springer (1986)"},{"key":"9255_CR37","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. arXiv:1106.3448v1 (2011). URL http:\/\/arXiv.org\/abs\/1106.3448"},{"key":"9255_CR38","unstructured":"le Rond D\u2019Alembert, J.: Recherches sur la courbe que forme une corde tendue mise en vibrations. In: Histoire de l\u2019Acad\u00e9mie Royale des Sciences et Belles Lettres (Ann\u00e9e 1747), vol. 3, pp. 214\u2013249. Haude et Spener, Berlin (1749)"},{"key":"9255_CR39","doi-asserted-by":"crossref","unstructured":"Lee, G., Werner, B.: Proof-irrelevant model of CC with predicative induction and judgmental equality. Logical Methods in Computer Science 7(4) (2011)","DOI":"10.2168\/LMCS-7(4:5)2011"},{"key":"9255_CR40","unstructured":"Lelay, C., Melquiond, G.: Diff\u00e9rentiabilit\u00e9 et int\u00e9grabilit\u00e9 en Coq. Application \u00e0 la formule de d\u2019Alembert. In: 23\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs, pp. 119\u2013133. Carnac, France (2012)"},{"key":"9255_CR41","volume-title":"2nd International Workshop on Types for Proofs and Programs (TYPES 2002), LNCS, vol. 2646","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) 2nd International Workshop on Types for Proofs and Programs (TYPES 2002), LNCS, vol. 2646. Springer, Berg en Dal (2003)"},{"key":"9255_CR42","first-page":"1","volume-title":"Programming Languages meets Program Verification (PLPV)","author":"C March\u00e9","year":"2007","unstructured":"March\u00e9, C.: Jessie: an intermediate language for Java and C verification. In: Programming Languages meets Program Verification (PLPV), pp. 1\u20132. ACM, Freiburg (2007)"},{"key":"9255_CR43","unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. Ph.D. thesis, Universit\u00e9 Paris VI (2001)"},{"key":"9255_CR44","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-45685-6_17","volume-title":"15th International Conference on Theorem Proving and Higher-Order Logic, LNCS, vol. 2410","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., Mu\u00f1oz, C., Tahar, S. (eds.) 15th International Conference on Theorem Proving and Higher-Order Logic, LNCS, vol. 2410, pp. 246\u2013262. Springer, Hampton (2002)","edition":"2410"},{"key":"9255_CR45","doi-asserted-by":"crossref","unstructured":"Microprocessor Standards Committee: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008, pp. 1\u201358 (2008). doi: 10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"key":"9255_CR46","doi-asserted-by":"crossref","unstructured":"Newton, I.: Axiomata, sive Leges Motus. In: Philosophiae Naturalis Principia Mathematica, vol. 1. London (1687)","DOI":"10.5479\/sil.52126.39088015628399"},{"key":"9255_CR47","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201908), LNCS, vol. 5170, pp. 246\u2013261. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_21"},{"issue":"37","key":"9255_CR48","doi-asserted-by":"crossref","first-page":"3386","DOI":"10.1016\/j.tcs.2010.05.031","volume":"411","author":"R O\u2019Connor","year":"2010","unstructured":"O\u2019Connor, R., Spitters, B.: A computer-verified monadic functional implementation of the integral. Theor. Comp. Sci. 411(37), 3386\u20133402 (2010)","journal-title":"Theor. Comp. Sci."},{"issue":"5","key":"9255_CR49","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/0307-904X(85)90019-8","volume":"9","author":"EE Rosinger","year":"1985","unstructured":"Rosinger, E.E.: Propagation of round-off errors and the role of stability in numerical methods for linear and nonlinear PDEs. Appl. Math. Model. 9(5), 331\u2013336 (1985)","journal-title":"Appl. Math. Model."},{"issue":"3","key":"9255_CR50","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0307-904X(91)90025-K","volume":"15","author":"EE Rosinger","year":"1991","unstructured":"Rosinger, E.E.: L-convergence paradox in numerical methods for PDEs. Appl. Math. Model. 15(3), 158\u2013163 (1991)","journal-title":"Appl. Math. Model."},{"issue":"25\u201328","key":"9255_CR51","first-page":"2131","volume":"200","author":"CJ Roy","year":"2011","unstructured":"Roy, C.J., Oberkampf, W.L.: A comprehensive framework for verification, validation, and uncertainty quantification in scientific computing. Comput. Methods Appl. Mech. Eng. 200(25\u201328), 2131\u20132144 (2011)","journal-title":"Comput. Methods Appl. Mech. Eng."},{"key":"9255_CR52","unstructured":"Rudnicki, P.: An overview of the MIZAR project. In: Types for Proofs and Programs, pp. 311\u2013332 (1992)"},{"key":"9255_CR53","unstructured":"Szyszka, B.: An interval method for solving the one-dimensional wave equation. In: 7th EUROMECH Solid Mechanics Conference (ESMC2009). Lisbon, Portugal (2009)"},{"key":"9255_CR54","unstructured":"The Coq reference manual. URL http:\/\/coq.inria.fr\/refman\/"},{"key":"9255_CR55","unstructured":"The Frama-C platform for static analysis of C programs (2008). URL http:\/\/www.frama-c.cea.fr\/"},{"key":"9255_CR56","doi-asserted-by":"crossref","unstructured":"Thomas, J.W.: Numerical partial differential equations: finite difference methods. In: Texts in Applied Mathematics, no. 22. Springer (1995)","DOI":"10.1007\/978-1-4899-7278-1"},{"key":"9255_CR57","unstructured":"Zach, R.: Hilbert\u2019s \u201cVerunglueckter Beweis,\u201d the first epsilon theorem, and consistency proofs. URL http:\/\/front.math.ucdavis.edu\/math.LO\/0204255"},{"key":"9255_CR58","unstructured":"Zwillinger, D.: Handbook of Differential Equations. Academic Press (1998)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9255-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9255-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9255-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T16:27:56Z","timestamp":1562084876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9255-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,14]]},"references-count":58,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["9255"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9255-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,14]]}}}