P. Cousot, The Verification Grand Challenge and Abstract Interpretation

Patrick Cousot.
The Verification Grand Challenge and Abstract Interpretation.
In Verified Software: Tools, Theories, Experiments, Bertrand Meyer & Jim Woodcock (Eds), LNCS 4171, © Springer-Verlag, Berlin, pp. 227—240, Dec. 2007.
PDF (160 Kb)
Abstract:
     Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science. The scope of application is rather large e.g.\ from type inference, model-checking, program transformation, watermarking to context-free grammar parser generation.
     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, ASTRÉE can analyze mechanically and verify formally the absence of runtime errors in industrial safety-critical embedded synchronous control/command codes of several hundred thousand to one million of lines 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.
Keywords:
Abstract Interpretation, Grand Challenge, Software, Static Analysis, Verification.

Bibliographic reference:

\bibitem{Cousot07-VSTTE}
P. Cousot.
\newblock The Verification Grand Challenge and Abstract Interpretation.
\newblock In \emph{Verified Software: Theories, Tools, Experiments}, B.\
	  Meyer \& J.\ Woodcock (Eds), pages 227--240, Lecture Notes in
	  Computer Science, volume 4171, Springer, Berlin, Dec. 2007.

@inCollection{Cousot07-VSTTE,
   author =    {Cousot, P{.}},
   title =     {The Verification Grand Challenge and Abstract 
                Interpretation},
   booktitle = {Verified Software: Theories, Tools, Experiments},
   editor =    {B.\ Meyer and J.\ Woodcock},
   year =      2007,
   series =    {Lecture Notes in Computer Science},
   month =     dec,
   volume =    {4171},
   pages =     {227--240},
   publisher = {Springer, Berlin, Germany},
}

copyright notice, Springer copyright
Last modified: Friday, 04-May-2012 10:02:50 EDT