Hardware-Dependent Proofs of Numerical Programs

Thi Minh Tuyen Nguyen 1, 2 Claude Marché 1, 2
2 PROVAL - Proof of Programs
CNRS - Centre National de la Recherche Scientifique : UMR, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France
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


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

200

Téléchargements du document

138