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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Boldo, S. (2009). Floats and ropes: A case study for formal numerical program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5556 LNCS, pp. 91–102). https://doi.org/10.1007/978-3-642-02930-1_8
Mendeley helps you to discover research relevant for your work.