Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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)
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, June 21, 2011 - 9:57:18 PM
Last modification on : Friday, October 28, 2022 - 3:28:52 AM
Long-term archiving on: : Friday, November 9, 2012 - 4:46:44 PM


Files produced by the author(s)


  • HAL Id : inria-00602266, version 1


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⟩



Record views


Files downloads