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.

\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,
}