CANUM 2020 : mini-symposium "Certification numérique"

Description

Le calcul numérique est un outil largement utilisé, que ce soit pour l'automatisation de tâches, pour la prédiction de phénomènes physiques, ou encore pour le développement de procédés industriels. Pour autant, l'accumulation des d'erreurs, dues à la fois à la troncature de l'arithmétique flottante, à la précision de l'approximation discrète, en particulier dans un contexte non linéaire, et à la qualité de l'implémentation informatique, impacte directement la fiabilité de ces outils.

Afin d’évaluer leur comportement, identifier les sources d'erreur et d'estimer ou de majorer la sensibilité numérique du système, on peut estimer, majorer, prouver des bornes sur ces erreurs, que ce soit de façon ad hoc, automatisée ou certifiée formellement.

L'objectif de ce mini-symposium est de mettre en avant différentes méthodes permettant de contrôler ces erreurs pendant la simulation et d’en montrer l'usage dans des applications pratiques. L'arithmétique flottante et les méthodes seront présentées, avec les techniques de preuves en Coq. Ce sera complété par des exposés de l'utilisation de ces techniques en analyse numérique (EDP, filtres) pour le contrôle des erreurs.