Hardware-Dependent Proofs of Numerical Programs

Thi Minh Tuyen Nguyen 1, 2 Claude Marché 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 : We present an approach for proving behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computa- tions. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. The approach is implemented on top of the generic Why platform for deductive verifi cation, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00772508
Contributeur : Claude Marché <>
Soumis le : mardi 19 février 2013 - 15:06:28
Dernière modification le : jeudi 9 février 2017 - 15:58:04
Document(s) archivé(s) le : lundi 20 mai 2013 - 03:59:00

Fichier

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

Identifiants

  • HAL Id : hal-00772508, version 1

Collections

Citation

Thi Minh Tuyen Nguyen, Claude Marché. Hardware-Dependent Proofs of Numerical Programs. Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011. 〈hal-00772508〉

Partager

Métriques

Consultations de
la notice

241

Téléchargements du document

153