Sites Inria

Conference

Exposé Xavier Leroy : À la recherche de la perfection logicielle

Xavier Leroy, responsable de l'équipe-projet Gallium du centre de recherche Inria de Paris © Inria / Photo G. Scagnelli

Xavier Leroy , directeur de recherche à Inria Paris est l’invité du prochain Colloquium du Loria. Il présentera son exposé intitulé “À la recherche de la perfection logicielle “.

Les personnes extérieures au centre souhaitant assister à cette présentation doivent s’inscrire par e-mail avant le mardi 22 mai.

  • Date : 25/05/2018
  • Lieu : Inria Nancy Grand Est
  • Intervenant(s) : Xavier Leroy, équipe Gallium Inria
  • Organisateur(s) : LORIA

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.

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !