Semaine 4 : Formal proof, Symbolic computation and Arithmetic of computers

Du 3 février 2014 au 7 février 2014

Mathematical Structures of Computation
Détails sur le site dédié

Thèmes abordés : preuves formelles en relation avec des questions d’arithmétique des ordinateurs et de calcul formel

Organisateurs :

Nicolas Brisebarre (CNRS, LIP, AriC INRIA Grenoble Rhône-Alpes, ÉNS de Lyon), Jean-Michel Muller (CNRS, LIP, AriC INRIA Grenoble Rhône-Alpes, ÉNS de Lyon).

40 participants

10 entretiens donnés par des experts en calcul numérique, preuve formelle, et le calcul symbolique. Cette semaine se veut une occasion unique pour développer et lancer de nouveaux projets autour des questions étroitement liées, à savoir, les preuves formelles d’opérations élémentaires d’arithmétique flottante ou des processus d’évaluation de la fonction, de la certification des approximations rationnelles / polynômes de solutions d’équations différentielles.

Beaucoup de systèmes critiques (c’est à dire lorsque la défaillance pourrait avoir des conséquences graves) dépendent en grande partie d’outils logiciels qui ont besoin d’être efficaces et parfaitement fiables (par exemples, dans la gestion des centrales nucléaires; les transports publics; les satellites, les hélicoptères assistée par ordinateur, etc.) Pour atteindre cet objectif de sécurité ultime assistée par ordinateur, l’utilisation de la preuve formelle s’est progressivement répandue, avec beaucoup de succès, dans des domaines tels que l’avionique. Toutefois, des difficultés majeures subsistent quand il s’agit de prouver formellement les nombreux algorithmes critiques et des codes numériques que nous rencontrons.