P. Cousot, Abstract interpretation with applications to semantics and static analysis

Patrick Cousot.
Abstract interpretation with applications to semantics and static analysis.
CS Colloquium, Departmental Seminar, Computer Science Department, Courant Institute of Mathematical Sciences, New York University, New York, NY, USA. April 9^th, 2007.
Abstract:
Abstract interpretation is a theory of sound approximation of mathematical structures, in particular those involved in the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model-checking, static analysis, program transformation and optimization, typing, software steganography, malware detection, etc.). Its main current application is on the safety and security of complex hardware and software computer systems.
After a brief formal introduction to abstract interpretation, we present two applications. The first theoretical application is to the design of several semantics of the eager lambda-calculus. The second application is practical and concerns the verification of the absence of runtime errors in industrial safety-critical real-time synchronous control-command avionic software.
Slides of the 55 mn presentation: .pdf .

Bibliographic reference:

\bibitem{Cousot-NYU-2007-04-09}
P.~Cousot.
\newblock Abstract interpretation with applications to semantics and static analysis.
\newblock \emph{CS Colloquium, Departmental Seminar}, 
         New York University, NY, USA, April 9${^\mathrm{th}}$ 2007.

@inProceedings{Cousot-NYU-2007-04-09,
   author =    {P{.} Cousot},
   title =     {Abstract interpretation with applications to semantics and static analysis},
   booktitle = {CS Colloquium, Departmental Seminar},
   address =   {New York University, NY, USA},
   month =     {April 9${^\mathrm{th}}$},
   year =      2007,
}

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