Hardware-independent proofs of numerical programs

Sylvie Boldo 1, 2 Thi Minh Tuyen Nguyen 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
2 LRI - Laboratoire de Recherche en Informatique
Abstract : On recent architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved.
Document type :
Conference papers
César Muñoz. Second NASA Formal Methods Symposium (NFM 2010), Apr 2010, Washington D.C., United States. NASA/CP-2010-216215, pp.14-23, 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00534410
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 9, 2010 - 3:21:24 PM
Last modification on : Thursday, February 9, 2017 - 3:54:53 PM
Document(s) archivé(s) le : Friday, October 26, 2012 - 3:20:40 PM

File

index.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00534410, version 1

Collections

INRIA | UMR8623 | CENTRALESUPELEC

Citation

Sylvie Boldo, Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. César Muñoz. Second NASA Formal Methods Symposium (NFM 2010), Apr 2010, Washington D.C., United States. NASA/CP-2010-216215, pp.14-23, 2010. <inria-00534410>

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

269

Document downloads

126

Contact


archive-ouverte@inria.fr