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
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 computations. Direct analysis of the assembly code allows to accurately 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 verification, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.
Document type :
Reports
[Research Report] RR-7655, INRIA. 2011, pp.61
Liste complète des métadonnées


https://hal.inria.fr/inria-00602266
Contributor : Claude Marché <>
Submitted on : Tuesday, June 21, 2011 - 9:57:18 PM
Last modification on : Thursday, February 9, 2017 - 3:56:14 PM
Document(s) archivé(s) le : Friday, November 9, 2012 - 4:46:44 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00602266, version 1

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>

Share

Metrics

Record views

276

Document downloads

177