Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Wave equation numerical resolution: a comprehensive mechanized proof of a C program

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.
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 : lundi 16 novembre 2020 - 13:06:03
Archivage à long terme 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

1978

Téléchargements de fichiers

1626