| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
Floats & Ropes: a case study for formal numerical program verification
Abstract : We present a case study of a formal verification of a numerical program that computes the discretization of a simple partial differential equation. Bounding the rounding error was tricky as the usual idea, that is to bound the absolute value of the error at each step, fails. Our idea is to find out a precise analytical expression that cancels with itself at the next step, and to formally prove the correctness of this approach.
https://hal.inria.fr/inria-00432718
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 17, 2009 - 9:45:42 AM
Last modification on : Tuesday, December 8, 2020 - 10:32:10 AM
Contributor : Sylvie Boldo <>
Submitted on : Tuesday, November 17, 2009 - 9:45:42 AM
Last modification on : Tuesday, December 8, 2020 - 10:32:10 AM
Links full text
