Sûreté numérique pour les preuves assistées par ordinateur – NuSCAP

Les vingt dernières années ont vu l'avènement des preuves assistées par ordinateurs en mathématiques, et ce phénomène prend de plus en plus d'importance. Elles mobilisent divers niveaux de sûreté numérique, depuis les calculs rapides et stables jusqu'à la preuve formelle des calculs. Cependant, les routines et outils nécessaires sont en général ad hoc, ou peu (voire non) disponibles. La question de la sûreté numérique est aussi devenue critique pour la conception d'algorithmes de guidage et de contrôle, rendus plus complexes du fait de l'autonomie croissante des satellites. Nous proposons de développer un ensemble de théorèmes, d'algorithmes et de développements logiciels qui permettent d'exécuter des calculs au niveau de sûreté désiré. Pour cela, nous concevrons notamment des méthodes spectrales et une arithmétique polynomiale rapides et certifiées, avec les formalisations correspondantes. Il y aura une interaction constante entre le développement de nos outils et le traitement des applications qui la motivent.