P. Cousot, Abstract Interpretation: Theory and Practice

Patrick Cousot.
Abstract Interpretation: Theory and Practice, Invited talk.
European Joint Conferences on Theory and Practice of Software (ETAPS 2002), Grenoble, France, Friday, April 12, 2002.
Abstract:      Our objective in this talk is to give an intuitive account of abstract interpretation theory and to present and discuss its main applications.
     Abstract interpretation theory formalizes the conservative approximation of the semantics of hardware or software computer systems. The \emph{semantics} provides a formal model describing all possible behaviors of a computer system in interaction with any possible environment. By \emph{approximation} we mean the observation of the semantics at some level of abstraction, ignoring irrelevant details. \emph{Conservative} means that the approximation can never lead to an erroneous conclusion.
     Abstract interpretation theory provides \emph{thinking tools} since the idea of abstraction by conservative approximation is central to reasoning (in particular on computer systems) and \emph{mechanical tools} since the idea of an effectively computable approximation leads to a systematic and constructive formal design methodology of automatic semantics-based program manipulation algorithms and tools.
     We will present various applications of abstract interpretation theory to the design of hierarchies of semantics, program transformations, typing, model-checking and in more details static program analysis. Abstract interpretation provides a general theory behind all program analyzers, which only differ in their choice of considered programming languages, program properties and their abstractions. Finally, we will discuss the various possible designs of program analyzers, from general-purpose to application-specific ones.
Slides of the 60mn talk: pdf.gz

Bibliography:

\bibitem{Cousot02-ETAPS02}
P{.} Cousot.
\newblock Abstract Interpretation: Theory and Practice, Invited talk.
\newblock \emph{European Joint Conferences on Theory and Practice of
          Software} (ETAPS 2002), Grenoble, France, Friday, April 12, 2002.

@unpublished{Cousot02-ETAPS02,
   author =  {P{.} Cousot},
   title = {Abstract Interpretation: Theory and Practice, Invited talk},
   note = {\emph{European Joint Conferences on Theory and Practice of
           Software} (ETAPS 2002), Grenoble, France, Friday, April 12, 2002},
}

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