In particular, abstract interpretation-based static analysis, which automatically infers dynamic properties of computer systems, has been very successful these last years to automatically verify complex properties of real-time, safety critical, embedded systems.

     For example, the static analyzer ASTRÉE can analyze mechanically and verify formally the absence of runtime errors in industrial safety-critical embedded control/command codes of several hundred thousand lines of C. We summarize the main reasons for the technical success of ASTRÉE, which provides directions for application of abstract interpretation to the Verification Grand Challenge.

• A4 landscape .pdf.gz (268 Kb) to be gunzip'ed for viewing with Acrobate Reader and compressed PostScript .ps.gz (2.1 Mb) for viewing with Ghostview or printing; LI> 2 slides per A4 landscape page .pdf.gz (188 Kb) for viewing with Acrobate Reader and compressed PostScript .ps.gz (1.1 Mb) for viewing with Ghostview or printing;
• 4 slides per A4 landscape sheet for printing in color (1 Mb) or black & white (680 Kb).

\bibitem{Cousot05-VSTTE}
P.~Cousot.
\newblock The Verification Grand Challenge and Abstract Interpretation.
\newblock In \emph{Verified Software: Theories, Tools, Experiments (VSTTE)}, 
          ETH Z{\"u}rich, Switzerland, October 10th--13th, 2005.

@inproceedings{Cousot05-VSTTE,
   author =    {Cousot, P{.}},
   title =     {The Verification Grand Challenge and Abstract Interpretation},
   booktitle = {Verified Software: Theories, Tools, Experiments (VSTTE)},
   address =   {ETH Z\"urich, Switzerland},
   month =     oct # " 10--13",
   year =      2005,
}