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
* Auteur correspondant
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : 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.
Type de document :
Article dans une revue
Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. <10.1016/j.camwa.2014.06.004 >
Liste complète des métadonnées


https://hal.inria.fr/hal-00769201
Contributeur : Francois Clement <>
Soumis le : lundi 2 juin 2014 - 12:58:39
Dernière modification le : jeudi 9 février 2017 - 15:57:38
Document(s) archivé(s) le : mardi 11 avril 2017 - 02:43:08

Fichiers

RR-8197.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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 and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. <10.1016/j.camwa.2014.06.004 >. <hal-00769201v3>

Partager

Métriques

Consultations de
la notice

602

Téléchargements du document

580