-
Recherche
- Présentation
- Trimestres et mois thématiques
- Evénements scientifiques
-
Chercheurs invités
- Chercheurs invités 2021
- Chercheurs invités 2022
- Chercheurs invités 2023
-
Post-doctorants Milyon
- Post-doctorants 2022
- Post-doctorants 2023
- Publications
- Prix, honneurs, bourses de recherche
- Portraits de chercheurs
- Formation
- Médiation
- Entreprise
- Appels à candidature
- Contacts
Vous êtes ici : Version française > Présentation > Trimestres et mois thématiques
-
Partager cette page
Semaine 4 : Formal proof, Symbolic computation and Arithmetic of computers
Du 3 février 2014 au 7 février 2014
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.