Chargement Évènements

« Tous les Évènements

  • Cet évènement est passé

Colloquium Loria : Xavier Leroy

mai 25 @ 13:30 - 14:30

Le vendredi 25 mai à 13h30 aura lieu le Colloquium du Loria avec Xavier Leroy, directeur de recherche Inria Paris.

Son exposé s’intitule “À la recherche de la perfection logicielle”.

Résumé :

Pour le grand public, le mot “logiciel” est devenu synonyme de “bug” et de “faille de sécurité”. Pourtant, il existe des logiciels critiques, dont dépendent des vies humaines, qui atteignent un extraordinaire niveau de fiabilité.
Prenant l’exemple des logiciels avioniques de commandes électroniques de vol, je montrerai quelques unes des techniques qui mènent à cette fiabilité. L’une d’entre elles passe par l’utilisation de méthodes formelles automatisées par des outils de vérification (analyse statique, preuve de programmes, vérification par modèles) en complément, et parfois en remplacement, des méthodes traditionnelles de vérification à base de tests.
Cependant, les garanties fournies par la vérification formelle sont limitées par la confiance que nous pouvons avoir envers les outils de vérification et envers les compilateurs et générateurs automatiques de code qui produisent le vrai code exécutable à partir du code source qui a été vérifié. En m’appuyant sur l’exemple du compilateur C vérifié CompCert, je montrerai l’intérêt et l’efficacité de vérifier formellement, à l’aide d’assistants de preuve, les outils qui sont impliqués dans la construction et la vérification du logiciel critique.

Les personnes extérieures au laboratoire doivent s’inscrire par e-mail avant le mardi 22 mai.

Détails

Date :
mai 25
Heure :
13:30 - 14:30
Catégorie d’Évènement:

En ce moment

Colloquium Loria 2018

Exposés précédents

Logo du CNRS
Logo Inria
Logo Université de Lorraine