Formal Proof of a Wave Equation Resolution Scheme: the Method Error

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
* Auteur correspondant
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
5 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Résumé : Les schémas numériques de résolution de l'équation des ondes en dimension 1 sont notoirement convergents. Nous présentons une formalisation détaillée du schéma le plus simple et nous prouvons formellement sa convergence dans le système d'aide à la preuve Coq. La difficulté principale se situe dans la définition adéquate des comportements asymptotiques et du fait que ces comportements ne sont pas complètement décrits dans les preuves sur papier. À notre connaissance, c'est la première mécanisation complète d'une telle preuve en analyse numérique.
Type de document :
Communication dans un congrès
Matt Kaufmann and Lawrence C. Paulson. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.147-162, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_12〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00450789
Contributeur : Francois Clement <>
Soumis le : mercredi 11 mai 2011 - 17:14:01
Dernière modification le : mardi 16 janvier 2018 - 14:46:17
Document(s) archivé(s) le : vendredi 12 août 2011 - 02:40:07

Fichiers

RR-7181.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.. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. Matt Kaufmann and Lawrence C. Paulson. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.147-162, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_12〉. 〈inria-00450789v3〉

Partager

Métriques

Consultations de la notice

1185

Téléchargements de fichiers

201