Proving Floating-Point Numerical Programs by Analysis of their Assembly Code

Nguyen Thi Minh Tuyen 1, 2 Claude Marché 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Nous décrivons une nouvelle approche pour prouver des propriétés du comportement des programmes numériques en analysant leur code assembleur compilé. Nous mettons l'accent sur les enjeux et les pièges qui peuvent survenir lors des calculs en virgule flottante. L'analyse directe du code assembleur permet de prendre en compte de façon précise l'architecture et le compilateur, par exemple l'utilisation de registres en précision flottante étendue. Un prototype est implanté au-dessus de la plate-forme générique \Why plate-forme pour la vérification déductive. Nous présentons des expérimentations où les preuves sont effectuées par une combinaison de plusieurs prouveurs automatiques.
Type de document :
Rapport
[Research Report] RR-7655, INRIA. 2011, pp.61
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00602266
Contributeur : Claude Marché <>
Soumis le : mardi 21 juin 2011 - 21:57:18
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 9 novembre 2012 - 16:46:44

Fichier

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

Identifiants

  • HAL Id : inria-00602266, version 1

Collections

Citation

Nguyen Thi Minh Tuyen, Claude Marché. Proving Floating-Point Numerical Programs by Analysis of their Assembly Code. [Research Report] RR-7655, INRIA. 2011, pp.61. 〈inria-00602266〉

Partager

Métriques

Consultations de la notice

325

Téléchargements de fichiers

222