Trusting computations: a mechanized proof from partial differential equations to actual program

Sylvie Boldo (1, 2) , François Clément (3) , Jean-Christophe Filliâtre (1, 2) , Micaela Mayero (4) , Guillaume Melquiond (1, 2) , Pierre Weis (3)

1 LRI - Laboratoire de Recherche en Informatique
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
3 POMDAPI - Environmental Modeling, Optimization and Programming Models
4 LIPN - Laboratoire d'Informatique de Paris-Nord

Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.

Les programmes peuvent échouer, que ce soit en raison de comportements exceptionnels, d'accès hors des bornes d'un tableau, ou simplement d'erreurs de codage. On ne peut donc pas leur faire confiance aveuglément. De ce point de vue, les programmes de calcul scientifique ne font pas exception, et ils présentent même des problèmes spécifiques de précision en raison de l'utilisation massive de calculs en virgule flottante. Cependant, leur correction est rarement garantie. En effet, nous avons dû étendre des méthodes et des outils existants pour prouver le comportement correct de programmes pour vérifier un programme d'analyse numérique existant. Ce programme C implémenté le schéma explicite aux différences finies centrées du second ordre pour la résolution de l'équation des ondes mono-dimensionnelle. En fait, nous sommes allés beaucoup plus loin puisque nous avons vérifié mécaniquement la convergence du schéma numérique pour obtenir une preuve formelle complète couvrant tous les aspects de l'équation aux dérivées partielles aux résultats numériques effectifs. À notre connaissance, c'est la première fois qu'une telle preuve complète est obtenue.

Mots clés: Rounding error analysis; Convergence of numerical scheme; Formal proof of numerical program; Acoustic wave equation

Domaines: Analyse numérique [math.NA]; Logique en informatique [cs.LO]

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Trusting computations: a mechanized proof from partial differential equations to actual program. Computers & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩. ⟨hal-00769201v3⟩