P. Cousot, Abstract Interpretation and Static Analysis

Patrick Cousot.
Abstract Interpretation and Static Analysis.
40th Meeting of the IFIP Working Group 10.4 on “Dependable computing and fault tolerance”, Stenungsund, Sweden, 4-8 July, 2001.
Abstract: After introductory motivations on software reliability, we survey the theoretical and practical limitations of software verification/validation formal methods, which are all necessarily approximate, as formalized by abstract interpretation.
   We then provide the intuition for the theory of abstract interpretation. The notion of abstraction is illustrated on effective numerical and symbolic abstractions which are shown to be conservative approximations in that the information loss never leads to erroneous conclusions (such as false positive or false negative). We then introduce the notion of abstraction of properties, fonctions and fixpoints, whether exact or approximate.
   In the second part of the talk, we consider applications of abstract interpretation which are introduced informally through examples.
   As an example of exact abstraction, we consider the design of a hierarchy of semantics.
   We then provide several examples of approximate abstractions, as used in static program analysis, abstract program checking and abstract program testing.
   Static program analysis is the automatic static determination of dynamic run-time properties of programs. The principle is to effectively compute an approximate semantics of the program. Abstract interpretation is used to derive,from a standard semantics,the approximate and computable abstract semantics. This is illustrated on the classical interval analysis (with widening/narrowing).
   We then consider static program analysis based software verification/validation. In abstract checking, the specification is derived automatically from the program (e.g. using the language specification for run-time errors). In abstract testing, the specification provided by the programmer.
   Finally, we provide refeences on abstract interpretation, its industrialization and its use in the DAEDALUS european project.
This presentation mainly relies on a paper available online: Patrick Cousot.
Abstract Interpretation Based Formal Methods and Future Challenges.
In Informatics, 10 Years Back - 10 Years Ahead, R. Wilhelm (Ed.), Lecture Notes in Computer Science 2000, pp. 138-156, 2001.
Slides of the 75mn presentation are available in .pdf (1 Mo).

\bibitem{Cousot01-WG10.4-Talk}
P{.} Cousot.
\newblock Abstract Interpretation and Static Analysis.
\newblock 40th Meeting of the IFIP Working Group 10.4 on ``Dependable
computing and fault tolerance'', Stenungsund, Sweden, 4-8 July, 2001.

@unpublished{Cousot01-WG10.4-Talk,
   author = {Cousot, P{.}},
   title =  {Abstract Interpretation and Static Analysis},
   note =   {40th Meeting of the IFIP Working Group 10.4 on ``Dependable 
             computing and fault tolerance'', Stenungsund, Sweden},
   month =  {4-8 jul},
   year =   2001,
}

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