| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Hardware-independent proofs of numerical programs
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.
Cited literature [18 references]
https://hal.inria.fr/inria-00534410
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 9, 2010 - 3:21:24 PM
Last modification on : Wednesday, September 16, 2020 - 5:04:54 PM
Long-term archiving on: : Friday, October 26, 2012 - 3:20:40 PM
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 9, 2010 - 3:21:24 PM
Last modification on : Wednesday, September 16, 2020 - 5:04:54 PM
Long-term archiving on: : Friday, October 26, 2012 - 3:20:40 PM
File
index.pdf
Files produced by the author(s)