Vérification de logiciels critiques

[English] [Index]
Étant donné les conséquences catastrophiques d'une erreur dans un logiciel critique, embarqué dans une voiture ou un avion par exemple, la vérification et la validation est particulièrement importante pour de tels logiciels. L'analyse statique est utile pour atteindre cet objectif, puisqu'elle peut donner des preuves que le logiciel satisfait les propriétés désirées.

Toute l'équipe interprétation abstract de l'École Normale Supérieure, avec Radhia Cousot de l'École Polytechnique, ont conçu et implémenté un analyseur qui verifie l'absence d'erreurs à l'exécution (division par zéro, dépassements de capacité, etc) dans des programmes C. Cet analyseur est efficace (1h40min pour analyser un programme industriel d'environ 75000 lignes) et atteint un niveau de précision sans précédent (seulement 11 fausses alarmes sur ce programme). Ce travail est fait dans le cadre du projet Astrée, en collaboration avec Airbus France.

Page officielle sur le projet Astrée

Publications sur ce sujet

[1]
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A Static Analyzer for Large Safety-Critical Software. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196-207, San Diego, California, June 2003. ACM.

[2]
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In T. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of Lecture Notes in Computer Science, pages 85-108. Springer, December 2002.


Bruno Blanchet