Appears in collections : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification, Exposés de recherche

From a (partial) differential equation to an actual program is a long road. This talk will present the formal verification of all the steps of this journey. This includes the mathematical error due to the numerical scheme (method error), that is usually bounded by pen-and-paper proofs. This also includes round-off errors due to the floating-point computations. The running example will be a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. This program is annotated to specify both method error and round-off error, and formally verified using interactive and automatic provers. Some work in progress about the finite element method will also be presented.