Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, February 19, 2013 - 3:06:28 PM
Last modification on : Sunday, June 26, 2022 - 11:57:47 AM
Long-term archiving on: : Monday, May 20, 2013 - 3:59:00 AM


Files produced by the author(s)


  • HAL Id : hal-00772508, version 1



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



Record views


Files downloads