Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

Sylvie Boldo 1, 2 François Clément 3 Jean-Christophe Filliâtre 1, 2 Micaela Mayero 4, 5 Guillaume Melquiond 1, 2 Pierre Weis 3
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
5 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Résumé : Nous prouvons formellement la correction d'un programme C implémentant un schéma numérique pour la résolution de l'équation des ondes acoustiques en dimension 1. Une telle implémentation introduit différents types d'erreurs : l'erreur de méthode due au schéma numérique et l'erreur d'arrondi due aux calculs en virgule flottante. Nous annotons ce programme C pour spécifier ces deux types d'erreur. Nous utilisons Frama-C pour générer les théorèmes qui garantissent la correction du code. Nous prouvons ces théorèmes à l'aide de solveurs SMT, de Gappa et de Coq. Un développement Coq important est nécessaire pour prouver l'adéquation du programme C au schéma numérique et pour borner les erreurs. À notre connaissance, c'est la première fois qu'un tel programme d'analyse numérique est complètement vérifié mécaniquement.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. 〈10.1007/s10817-012-9255-4〉
Liste complète des métadonnées

Littérature citée [52 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00649240
Contributeur : Francois Clement <>
Soumis le : jeudi 12 juillet 2012 - 10:41:13
Dernière modification le : vendredi 10 novembre 2017 - 14:52:01
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 22:36:35

Fichiers

RR-7826.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.. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. 〈10.1007/s10817-012-9255-4〉. 〈hal-00649240v3〉

Partager

Métriques

Consultations de
la notice

1268

Téléchargements du document

439