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.
Type de document :
Communication dans un congrès
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
https://hal.inria.fr/inria-00534410
Contributeur : Sylvie Boldo
<>
Soumis le : mardi 9 novembre 2010 - 15:21:24
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:20:40
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〉
