Verification of critical software
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