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

 Summary

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.

 Infos

 Downloads

 Embed/Share

Social Networks

 Options
Check the box to autoplay the video.
Check the box to loop the video.
Check the box to indicate the beginning of playing desired.
 Embed in a web page
 Share the link
qrcode