Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Parabolic maximal regularity applied to diffusion networks with time-dependent transmission conditions
De Wolfgang Arendt
De Sylvie Boldo
Apparaît dans les 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.