Computer Science Colloquium

Abstract interpretation with applications to semantics and static analysis

Patrick Cousot
École Normale Supérieure

Monday, April 9th 11:15 a.m.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Host/s:

Amir Pnueli amir@cs.nyu.edu, (212) 998-3225

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.

Refreshments will be served


top | contact webmaster@cs.nyu.edu