Proofs of numerical programs when the compiler optimizes

Sylvie Boldo 1, 2 Thi Minh Tuyen Nguyen 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : On certain recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers.We propose an approach that states the rounding error of each floatingpoint computation whatever the environment and the compiler choices. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved.
Type de document :
Article dans une revue
Innovations in Systems and Software Engineering, Springer Verlag, 2011, 7, pp.151-160
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00777639
Contributeur : Claude Marché <>
Soumis le : jeudi 21 février 2013 - 07:08:56
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : samedi 1 avril 2017 - 06:52:22

Fichier

ISSE.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-00777639, version 1

Collections

Citation

Sylvie Boldo, Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, Springer Verlag, 2011, 7, pp.151-160. 〈hal-00777639〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

523