| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
Proofs of numerical programs when the compiler optimizes
Abstract : On certain recently developed 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 floatingpoint computation whatever the environment and the compiler choices. 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 [24 references]
https://hal.inria.fr/hal-00777639
Contributor : Claude Marché <>
Submitted on : Thursday, February 21, 2013 - 7:08:56 AM
Last modification on : Wednesday, September 16, 2020 - 5:08:04 PM
Long-term archiving on: : Saturday, April 1, 2017 - 6:52:22 AM
Contributor : Claude Marché <>
Submitted on : Thursday, February 21, 2013 - 7:08:56 AM
Last modification on : Wednesday, September 16, 2020 - 5:08:04 PM
Long-term archiving on: : Saturday, April 1, 2017 - 6:52:22 AM
File
ISSE.pdf
Publisher files allowed on an open archive