P. Cousot, Abstract Interpretation

Patrick Cousot.
Abstract Interpretation.
Summer School on Theory and Practice of Language Implementation, University of Oregon, Eugene, Oregon, USA, 23—31 July, 2009.
Objectives:
     The verification of program properties being undecidable, all approaches have limitations. Either human help is required (to provide test cases, a finite model, or help in theorem proving) or tools fail to prove automatically that some program properties do hold (this is "incompleteness"). But for tiny programs for which exhaustive exploration is possible, the main difficulty is therefore to scale up. Faced with this situation, compromises have to be found to make practical automatic verification tools. One solution is to allow for non-termination, or memory usage explosion, for which it is impossible to know if a correctness proof could have been found with just a little more resources. Another compromise is to abandon soundness which essentially means that possible complex behaviors of the program to be verified are simply ignored e.g. by exploring the beginning of executions only or ignoring some or most of them. This does help in discovering bugs but not in proving their absence. Most tools are both incomplete and unsound, hence are debugging aids rather than correctness certification tools.
     Abstract interpretation aims at discovering and proving model or program properties by sound approximations of their behaviors which are computable with finite resources hence are necessarily incomplete. This means that abstract interrpetation-based verifiers may produce false alarms when mathematically true program properties are signaled as not proved. The design objective is therefore to find a balance between precision of the analysis (to minimize false alarms) and its cost (to make it usable in practice).
     The course sketches the principle of abstract interpretation where program analyzers are designed by sound approximation of the program properties. It explores practical a few applications of abstraction where the verification of specific classes of program properties has shown to be possible in practice with no or few alarms for very large programs.
Content:
Course documentation: The following reference is provided as a written pedagogical support for this course:
- Patrick Cousot & Radhia Cousot.
  Basic Concepts of Abstract Interpretation.
  In Building the Information Society , René Jacquard (Ed.), Kluwer Academic Publishers, pp. 359—366, 2004. (IFIP WCC 2004 Toulouse, Topical Day on Abstract Interpretation, Tuesday 24 August 2004).
The lessons are based on various papers which are available online.

Bibliography (to reference the course):

\bibitem{Cousot09-OREGON}
P{.} Cousot.
\newblock Abstract Interpretation.
\newblock \emph{Summer School on Theory and Practice of Language 
          Implementation},
          University of Oregon, Eugene, Oregon, USA, 23--31 July 2009,

@unpublished{Cousot09-OREGON,
   author = {P{.} Cousot},
   title  = {Abstract Interpretation},
   note =   {\emph{Summer School on Theory and Practice of Language 
            Implementation}},
  address = {University of Oregon, Eugene, Oregon, USA},
  month =   {23--31 July},
  year =    2009,
}

droits d'auteur, copyright notice.
Last modified: Friday, 01-Jan-2010 21:59:27 CET