ELFIC
Formal Verification of Finite Element Method Programs
(Programmes d’éléments finis formellement vérifiés)
|
Axis: SciLex 2&3 Coordinator : Sylvie Boldo, Inria Goal : Correctness proof of the FELiScE library that implements the finite element method for the numeric resolution of partial differential equations Scientific productions : Coq proofs and article Labex Funding in : 2014/2015 et 2015/2016 |
|
Documents : Link to the submitted project
Présentation:
Project ELFIC focuses on proving the correction of the FELiScE library (Finite Elements for Life Sciences and Engineering), which implements the finite element method for approximating solutions to partial differential equations. Finite elements are at the heart of numerous simulation programs used in industry. The Felisce C++ library is being developed at Inria and used for academic research; its formal verification will greatly increase confidence in all the programs that rely on it. Verification methods developed in this project will be a breakthrough for the finite element method, but more generally for the reliability of critical software relying on complicated numerical algorithms.
Teams
- Inria Saclay - Île-de-France, team Toccata: Sylvie Boldo, Claude Marché, Guillaume Melquiond
- Ecole Polytechnique, LIX: Eric Goubault, Sylvie Putot
- CEA LIST: Franck Védrine, Virgile Prévosto
- Inria Paris - Rocquencourt, team Pomdapi: François Clément, Pierre Weis
- Université Paris 13, LIPN (Laboratoire d’informatique de Paris Nord): Micaela Mayero
- UTC, LMAC (Laboratoire de Mathématiques Appliquées de Compiègne): Vincent Martin
Invited speaker:
- 19/05/15 : Numerical theorem proving using polynomial interval arithmetic (Michal Konečný, Aston University, Birmingham, UK)- PCRI/Ada Lovelace 650