Loading...
 
[Show/Hide Left Column]

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
Image


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