Multi angle Formal verification of numerical analysis programs
Auteurs : Boldo, Sylvie (Auteur de la Conférence)
CIRM (Editeur )
Loading the player...
Résumé : 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.Codes MSC :
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.
65G50 - Roundoff error
68N15 - Programming languages
68Q60 - Specification and verification (program logics, model checking, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65Y04 - Algorithms for computer arithmetic, etc.