Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

Sylvie Boldo 1, 2 François Clément 3, * Jean-Christophe Filliâtre 1, 2 Micaela Mayero 4 Guillaume Melquiond 1, 2 Pierre Weis 3
* Corresponding author
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.
Document type :
Journal articles
Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. <10.1016/j.camwa.2014.06.004 >
Liste complète des métadonnées


https://hal.inria.fr/hal-00769201
Contributor : Francois Clement <>
Submitted on : Monday, June 2, 2014 - 12:58:39 PM
Last modification on : Thursday, February 9, 2017 - 3:57:38 PM
Document(s) archivé(s) le : Tuesday, April 11, 2017 - 2:43:08 AM

Files

RR-8197.pdf
Files produced by the author(s)

Identifiers

Citation

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. <10.1016/j.camwa.2014.06.004 >. <hal-00769201v3>

Share

Metrics

Record views

602

Document downloads

580