Wave equation numerical resolution: a comprehensive mechanized proof of a C program. (English) Zbl 1267.68208
Summary: We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 35L05 | Wave equation |
| 65M22 | Numerical solution of discretized equations for initial value and initial-boundary value problems involving PDEs |
| 65G50 | Roundoff error |
Keywords:
formal proof of numerical program; convergence of numerical scheme; proof of C program; Coq formal proof; acoustic wave equation; partial differential equation; rounding error analysisSoftware:
Flocq; cvc3; Caduceus; KRAKATOA; Isabelle/HOL; ASTREE; z3; Gappa; Why3; ACSL; Mizar; ACL2; CoqReferences:
| [1] | Achenbach, J.D.: Wave Propagation in Elastic Solids. North Holland, Amsterdam (1973) · Zbl 0268.73005 |
| [2] | Andrews, G.E., Askey, R., Roy, R.: Special Functions. Cambridge University Press, Cambridge (1999) · Zbl 0920.33001 |
| [3] | Askey, R., Gasper, G.: Certain rational functions whose power series have positive coefficients. Am. Math. Mon. 79, 327-341 (1972) · Zbl 0242.33023 · doi:10.2307/2978081 |
| [4] | Avigad, J., Donnelly, K.: A decision procedure for linear “Big O” equations. J. Autom. Reason. 38(4), 353-373 (2007) · Zbl 1122.03004 · doi:10.1007/s10817-007-9066-1 |
| [5] | Barrett, C., Tinelli, C.: CVC3. In: 19th International Conference on Computer Aided Verification (CAV ’07), LNCS, vol. 4590, pp. 298-302. Springer, Berlin (2007) · Zbl 1119.68005 |
| [6] | Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, 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 · Zbl 1230.76049 |
| [7] | Bécache, E.: Étude de schémas numériques pour la résolution de l’équation des ondes. Master Modélisation et simulation, Cours ENSTA (2009). URL http://www-rocq.inria.fr/ becache/COURS-ONDES/Poly-num-0209.pdf · Zbl 0242.33023 |
| [8] | Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. Springer (2004) · Zbl 1069.68095 |
| [9] | Bertot, Y.; Gonthier, G.; Ould Biha, S.; Pasca, I., Canonical big operators, 86-101 (2008), Montreal · Zbl 1165.68450 · doi:10.1007/978-3-540-71067-7_11 |
| [10] | 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/ |
| [11] | Boldo, S.: Preuves formelles en arithmétiques à virgule flottante. Ph.D. thesis, École Normale Supérieure de Lyon (2004) |
| [12] | Boldo, S., Floats & Ropes: a case study for formal numerical program verification, 91-102 (2009), Rhodos · Zbl 1248.65045 |
| [13] | Boldo, S.; Filliâtre, JC, Formal verification of floating-point programs, 187-194 (2007), France · doi:10.1109/ARITH.2007.20 |
| [14] | Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innovations Syst. Softw. Eng. 7(2), 151-160 (2011) · doi:10.1007/s11334-011-0151-6 |
| [15] | Boldo, S.; Filliâtre, JC; Melquiond, G.; Carette, J. (ed.); Dixon, L. (ed.); Coen, CS (ed.); Watt, SM (ed.), Combining Coq and Gappa for certifying floating-point programs, 59-74 (2009), ON, Canada · Zbl 1247.68232 |
| [16] | Boldo, S.; Clément, F.; Filliâtre, JC; Mayero, M.; Melquiond, G.; Weis, P.; Kaufmann, M. (ed.); Paulson, LC (ed.), Formal proof of a wave equation resolution scheme: the method error, 147-162 (2010), Edinburgh · Zbl 1291.68329 · doi:10.1007/978-3-642-14052-5_12 |
| [17] | Boldo, S.; Melquiond, G.; Antelo, E. (ed.); Hough, D. (ed.); Ienne, P. (ed.), Flocq: A unified library for proving floating-point algorithms in Coq, 243-252 (2011), Germany |
| [18] | Brekhovskikh, L.M., Goncharov, V.: Mechanics of Continua and Wave Dynamics. Springer (1994) · Zbl 0791.73001 |
| [19] | 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-69. Elsevier (2008) · Zbl 1277.68240 |
| [20] | Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) Colog’88, LNCS, vol. 417. Springer (1990) · Zbl 0722.03006 |
| [21] | Courant, R., Friedrichs, K., Lewy, H.: On the partial difference equations of mathematical physics. IBM J. Res. Develop. 11(2), 215-234 (1967) · Zbl 0145.40402 · doi:10.1147/rd.112.0215 |
| [22] | Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: ESOP, no. 3444 in LNCS, pp. 21-30 (2005) · Zbl 1108.68422 |
| [23] | Cruz-Filipe, L.; Geuvers, H. (ed.); Wiedijk, F. (ed.), A constructive formalization of the fundamental theorem of calculus (2002), Berg en Dal |
| [24] | Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. Trans. Math. Softw. 37(1), 1-20 (2010) · Zbl 1364.68328 · doi:10.1145/1644001.1644003 |
| [25] | Daumas, M., Rideau, L., Théry, L.: A generic library for floating-point numbers and its application to exact computing. In: TPHOLs, pp. 169-184 (2001) · Zbl 1005.68544 |
| [26] | Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: FMICS, LNCS, vol. 5825, pp. 53-69. Springer (2009) |
| [27] | de Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242-253 (2011) · Zbl 1367.65250 · doi:10.1109/TC.2010.128 |
| [28] | de Moura, L., Bjørner, N.: Z3, an efficient SMT solver. In: TACAS, Lecture Notes in Computer Science, vol. 4963, pp. 337-340. Springer (2008) |
| [29] | Dutertre, B.; Wright, J. (ed.); Grundy, J. (ed.); Harrison, J. (ed.), Elements of mathematical analysis in PVS, 141-156 (1996), Turku · Zbl 1543.68417 · doi:10.1007/BFb0105402 |
| [30] | Filliâtre, JC; Marché, C., The Why/Krakatoa/Caduceus platform for deductive program verification, 173-177 (2007), Berlin |
| [31] | 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’00), LNCS, vol. 1869, pp. 145-161. Springer (2000) · Zbl 0974.68186 |
| [32] | Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason. 27(4), 323-351 (2001) · Zbl 0991.03018 · doi:10.1023/A:1011908113514 |
| [33] | Geuvers, H.; Niqui, M.; Callaghan, P. (ed.); Luo, Z. (ed.); McKinna, J. (ed.); Pollack, R. (ed.), Constructive reals in Coq: axioms and categoricity, 79-95 (2002), Durham · Zbl 1054.03039 |
| [34] | Harrison, J.: Theorem Proving with the Real Numbers. Springer (1998) · Zbl 0932.68099 |
| [35] | 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’05), LNCS, vol. 3603, pp. 114-129. Springer (2005) · Zbl 1152.68520 |
| [36] | John, F.: Partial Differential Equations. Springer (1986) · Zbl 1209.68108 |
| [37] | Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. arXiv:1106.3448v1 (2011). URL http://arXiv.org/abs/1106.3448 · Zbl 1260.68378 |
| [38] | le Rond D’Alembert, J.: Recherches sur la courbe que forme une corde tendue mise en vibrations. In: Histoire de l’Académie Royale des Sciences et Belles Lettres (Année 1747), vol. 3, pp. 214-249. Haude et Spener, Berlin (1749) |
| [39] | Lee, G., Werner, B.: Proof-irrelevant model of CC with predicative induction and judgmental equality. Logical Methods in Computer Science 7(4) (2011) · Zbl 1237.03008 |
| [40] | Lelay, C., Melquiond, G.: Différentiabilité et intégrabilité en Coq. Application à la formule de d’Alembert. In: 23èmes Journées Francophones des Langages Applicatifs, pp. 119-133. Carnac, France (2012) |
| [41] | Letouzey, P.; Geuvers, H. (ed.); Wiedijk, F. (ed.), A new extraction for Coq (2003), Berg en Dal · Zbl 1023.68516 |
| [42] | Marché, C., Jessie: an intermediate language for Java and C verification, 1-2 (2007), Freiburg |
| [43] | Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. Ph.D. thesis, Université Paris VI (2001) |
| [44] | Mayero, M.; Tahar, S.; Carreño, V. (ed.); Muñoz, C. (ed.), Using theorem proving for numerical analysis (correctness proof of an automatic differentiation algorithm), 246-262 (2002), Hampton · Zbl 1013.68203 · doi:10.1007/3-540-45685-6_17 |
| [45] | Microprocessor Standards Committee: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008, pp. 1-58 (2008). doi:10.1109/IEEESTD.2008.4610935 |
| [46] | Newton, I.: Axiomata, sive Leges Motus. In: Philosophiae Naturalis Principia Mathematica, vol. 1. London (1687) · Zbl 0050.00201 |
| [47] | O’Connor, R.: Certified exact transcendental real number computation in Coq. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs’08), LNCS, vol. 5170, pp. 246-261. Springer (2008) · Zbl 1165.68466 |
| [48] | O’Connor, R., Spitters, B.: A computer-verified monadic functional implementation of the integral. Theor. Comp. Sci. 411(37), 3386-3402 (2010) · Zbl 1209.68108 · doi:10.1016/j.tcs.2010.05.031 |
| [49] | 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-336 (1985) · Zbl 0622.65072 · doi:10.1016/0307-904X(85)90019-8 |
| [50] | Rosinger, E.E.: L-convergence paradox in numerical methods for PDEs. Appl. Math. Model. 15(3), 158-163 (1991) · Zbl 0725.65085 · doi:10.1016/0307-904X(91)90025-K |
| [51] | 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-28), 2131-2144 (2011) · Zbl 1230.76049 · doi:10.1016/j.cma.2011.03.016 |
| [52] | Rudnicki, P.: An overview of the MIZAR project. In: Types for Proofs and Programs, pp. 311-332 (1992) |
| [53] | Szyszka, B.: An interval method for solving the one-dimensional wave equation. In: 7th EUROMECH Solid Mechanics Conference (ESMC2009). Lisbon, Portugal (2009) |
| [54] | The Coq reference manual. URL http://coq.inria.fr/refman/ |
| [55] | The Frama-C platform for static analysis of C programs (2008). URL http://www.frama-c.cea.fr/ |
| [56] | Thomas, J.W.: Numerical partial differential equations: finite difference methods. In: Texts in Applied Mathematics, no. 22. Springer (1995) · Zbl 0831.65087 |
| [57] | Zach, R.: Hilbert’s “Verunglueckter Beweis,” the first epsilon theorem, and consistency proofs. URL http://front.math.ucdavis.edu/math.LO/0204255 · Zbl 1069.03002 |
| [58] | Zwillinger, D.: Handbook of Differential Equations. Academic Press (1998) · Zbl 0912.34001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
