P. Cousot & R. Cousot, Abstract Interpretation Based Program Transformations

Patrick Cousot & Radhia Cousot.
Abstract Interpretation Based Program Transformations.
CLIP Lab, Departamento de Inteligencia Artificial, Facultad de Informática, Universidad Politécnica de Madrid, Madrid, Spain, Thursday September 12, 2002.
Abstract: The first part of the talk is a short introduction to abstract interpretation expalined in the context of program static analysis. We review the notions of conservative approximations and information loss, the formalization of fixpoint semantic approximations by Galois connections, the use of abstract interpretation as a thinking tool and its use to design mechanical tools based upon effectively computable approximations. This first part ends with a review of the main applications of abstract interpretation.
In the second part we present a new application of abstract interpretation to program transformation introduced at POPL '02. The objective is not to formalize the static program analyses used in offline program transformations, which is classical, but to formalize the program transformation itself as an abstract interpretation. Beyond correctness proofs, this new point of view leads to a program transformation design method which is rapidly illustrated on online and offline constant propagation. The main idea is to view the correspondance between syntax and semantics, the syntax and semantic transformations as well as the observational equivalence as abstractions. We conclude by discussing perspectives on using this new approach to the static (re-)analysis of transformed programs.
Slides of the 60mn talk are available in various formats:
- A4 landscape .pdf (700 ko) and compressed .pdf.gz (404 Ko) and for viewing with Acrobate Reader and compressed PostScript .ps.gz (456 Ko) for viewing with Ghostview or printing;
- 4 slides per A4 landscape sheet in PDF (636 Ko) and .ps.gz format for printing in color (444 Ko) or in black & white (436 Ko).

\bibitem{CousotCousot02-UMP}
P{.} Cousot and R{.} Cousot.
\newblock Abstract Interpretation Based Program Transformation.
\newblock \emph{CLIP Lab, Departamento de Inteligencia Artificial, Facultad
de Inform\'atica, Universidad Polit\'ecnica de Madrid}, Madrid, Spain,
Thursday September 12, 2002.

@unpublished{CousotCousot02-UMP,
   author =  {P{.} Cousot and R{.} Cousot},
   title = {Abstract Interpretation Based Program Transformation},
   note = {\emph{CLIP Lab, Departamento de Inteligencia Artificial, Facultad
   de Inform\'atica, Universidad Polit\'ecnica de Madrid}, Madrid, Spain,
   Thursday September 12, 2002},
}

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