Verification of critical software

[Français] [Index]
Given the consequences of an error in critical software, embedded into a car or a plane, verification and validation is particularly important for such software. Static analysis is useful to achieve this goal, since it can give proofs that the software satisfies the desired properties.

The whole abstract interpretation team of École Normale Supérieure, with Radhia Cousot from École Polytechnique, have designed and implemented an analyzer that verifies the absence of runtime errors (division by zero, overflows, etc) in C programs. This analyzer is efficient (1h40min to analyze an industrial program of about 75000 lines) and reaches an unprecedented level of precision (only 11 false alarms on this program). This work is done in the frame of the Astrée project, in collaboration with Airbus France.

Official Astrée project page

Publications on this topic

[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