Formal verification of tricky numerical computations

Sylvie Boldo 1, 2
1 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
Abstract : Computer arithmetic has applied formal methods and formal proofs for years. As the systems may be critical and as the properties may be complex to prove (many sub-cases, error-prone computations), a formal guarantee of correctness is a wish that can now be fulfilled. This talk will present a chain of tools to formally verify numerical programs. The idea is to precisely specify what the program requires and ensures. Then, using deductive verification, the tools produce proof obligation that may be proved either automatically or interac-tively in order to guarantee the correctness of the specifications. Many examples of programs from the literature will be specified and formally verified.
Type de document :
Communication dans un congrès
Marco Nehmeier. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39, 2014, 〈http://www.scan2014.uni-wuerzburg.de/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01088692
Contributeur : Sylvie Boldo <>
Soumis le : vendredi 28 novembre 2014 - 14:14:03
Dernière modification le : jeudi 9 février 2017 - 15:53:05
Document(s) archivé(s) le : vendredi 14 avril 2017 - 23:02:28

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01088692, version 1

Citation

Sylvie Boldo. Formal verification of tricky numerical computations. Marco Nehmeier. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39, 2014, 〈http://www.scan2014.uni-wuerzburg.de/〉. 〈hal-01088692〉

Partager

Métriques

Consultations de
la notice

195

Téléchargements du document

76