Xavier Leroy : "À la recherche de la perfection logicielle"

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.