• Patrick Cousot.
  Abstract Interpretation for Software Verification.
  Workshop on “Formal Design of Safety Critical Embedded Systems, FEmSys'2001”, Forum der Technik, Deutsches Museum, München, Germany, 21-23 March, 2001.

• Abstract: From a mathematical point of view, abstract interpretation formalizes the idea of approximation of sets and set operations as considered in set (or category) theory. From a computer science point of view, abstract interpretation is a theory of approximation of the semantics of programming languages. Its main application has been the formal design of static program analyzers aiming at inferring general runtime properties of programs statically, that is without executing them. Such fully automatic analyzers have been used successfully to track bugs in safety critical embedded systems and to verify the absence of runtime errors.

  The purpose of this talk is to explain the basic principles of abstract interpretation and to explain, in an informal way, how the concept of approximation, formalized by this theory, is central to all software verification methods (from debugging, to typing, model-checking and deductive methods). In abstract interpretation we consider safe approximations which provide a full coverage of all possible cases at run-time.

  Then, we sketch the application to the formal design of static program analyzers by compositional abstraction of a programming language semantics. The price to be paid for the effective static safe approximation of run-time properties is that of uncertainty. Practical analyzers have therefore to provide a good compromise between the cost of the analysis and its precision. We discuss various methods which can be used to obtain an acceptable balance.

  Finally, we explain an application of static program analysis to abstract testing, a version of interactive program debugging where the execution of programs on test values are replaced by the static checking of user provided program properties.

• 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 60mn presentation: .pdf.

A

\bibitem{Cousot01-FEmSys-Talk}
P{.} Cousot.
\newblock Abstract Interpretation for Software Verification.
\newblock Workshop on “Formal Design of Safety Critical Embedded
Systems, FEmSys'2001”, München, Germany, 21-23 March, 2001.


@unpublished{Cousot00-Dagstuhl-Talk,
   author =  {Cousot, P{.}},
   title =   {Abstract Interpretation for Software Verification},
   note =    {Workshop on “Formal Design of Safety Critical 
              Embedded Systems, FEmSys'2001”, München, 
              Germany},
   month =   {21--23 mar},
   year =    2001,
}