Dans de nombreuses applications, typiquement en automatique ou en robotique, ou encore lors de la mise au point de méthodes combinant à la fois des algorithmes symboliques et des algorithmes numériques, il est nécessaire d'obtenir une certitude quant à la précision du résultat d'un calcul matriciel effectué en arithmétique flottante.
De nombreuses bibliothèques pour les calculs matriciels ont été développées et sont sans cesse optimisées afin d'approcher les performances crêtes des machines : citons par exemple LAPACK, mais aussi les projets plus récents PLASMA et MAGMA, visant à atteindre les meilleures performances sur les architectures multicoeurs et hybrides CPU-GPU respectivement. Ces bibliothèques sont largement utilisées, mais elles ne fournissent qu'une estimation (parfois pessimiste, parfois erronée) de la précision de la solution calculée. En outre, ces bibliothèques ne prennent pas en compte les incertitudes sur les coefficients des matrices manipulées.
Le but des méthodes de vérification en arithmétique flottante est de mettre au point des algorithmes permettant de borner la précision du résultat, tout en assurant de bonnes performances lors de leur implantation en machine. De nombreuses méthodes sont notamment basées sur l'utilisation de l'arithmétique d'intervalles, qui fournit un encadrement de chacun des calculs intermédiaires ; les propriétés de l'arithmétique IEEE-754 peuvent également être exploitées directement afin d'améliorer les performances des algorithmes. De plus, lorsque la précision du résultat n'est pas suffisante, il convient de proposer des méthodes permettant de l'améliorer, tout en maintenant la contrainte de performances.
L'objectif de ce cours sera de dresser un état de l'art des méthodes de vérification existantes pour les algorithmes classiques en algèbre linéaire : produit de matrices, factorisations et résolution de systèmes linéaires. Les différentes étapes de ce cours consisteront à :