P. Cousot, Abstract Interpretation of Computations

Patrick Cousot.
Abstract Interpretation of Computations.
In Workshop on Robustness, Abstractions and Computations, University of Pennsylvania, Philadelphia, U.S.A., 28 March 2004.
Abstract:
     Following the exponential growth of hardware complexity, the current exponential expansion of software in all application domains, leads to the unfortunate situation where software engineers can build increasingly large software but are less and less confident in the quality of the software they build. Commercial software with more than one bug every thousand lines is not so uncommon. This situation is not tolerated in control/command systems involving large and complex real-time embedded safety critical software for which the development costs to achieve high-quality objectives are therefore rapidly becoming prohibitive. Because present-day engineering, which is almost exclusively manual, with very few automated tools, does not scale up, a grand challenge is therefore to develop knowledge, methods, technologies and tools to master software complexity.
     This means that one must be able to model the computations/executions of software in any possible environment (its so-called semantics) at various levels of abstraction. This is the purpose of abstract interpretation, a theory of the approximation of semantics aimed at supporting rigorous reasoning about software. Applications of abstract interpretation include proof methods as well as automatic software manipulation tools such as static analyzers. Static analyzers aim at proving properties of software execution using classes of conservative abstractions (that are simplifying approximations to cope with undecidability).
     The talk first introduce a few elements of the theory of abstract interpretation. We then shortly present the main applications of abstract interpretation. This includes the compositional reachability static analysis of a C-like imperative language in infinite abstract domains with convergence acceleration by widening.
     We then provide the example of ASTRÉE, a static analyzer developed at the École normale supérieure (www.astree.ens.fr) that was able to prove completely automatically the absence of any run-time error in the primary flight control software of the Airbus A340 fly-by-wire system.
     Finally, we rapidly review a few of the abstractions which have been used in ASTRÉE to achieve zero false alarm, a world première.
Slides of the 30mn presentation: .pdf.

Bibliography:

\bibitem{Cousot-RAC04}
P{.} Cousot.
\newblock Abstract Interpretation of Computations.
\newblock \emph{Workshop on Robustness, Abstractions and Computations}
 University of Pennsylvania, Philadelphia, U.S.A., 28 March 2004.

@conference{Cousot-RAC04,
   author =    {P{.} Cousot},
   title =     {Abstract Interpretation of Computations},
   booktitle = {Workshop on Robustness, Abstractions and Computations},
   address =   {University of Pennsylvania, Philadelphia, U.S.A.},
   month =     {28 March},
   year =      2004,
}

All presentations of the workshop

copyright notice.
Last modified: Monday, 07-May-2012 17:51:05 EDT