[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, June 1, 2005
11:45-1:15
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Patrick Cousot
Ecole Normale Superieure, Paris
Visiting MIT Aero-Astro Department

A basic property of software is that there should be no reachable
state of the computations in which an undefined operation can be
performed.  For example in synchronous software, as found in safety
critical embedded application such as electric flight control, a
runtime error might raise an interrupt whence break the synchrony.

The state space of such huge programs (hundreds of thousands of lines)
is so large that it cannot be explored explicitly by model-checking
nor reasonably covered by testing.  A (computer-aided) formal proof
would be humanely insurmountable and economically very costly.

An alternative is to use static analysis where an abstraction of the
semantics of the programs is automatically computed which leaves out
all information about reachable states which is not strictly necessary
for the proof.  Of course if the abstraction is too precise, the
computation cost are too high (resource exhaustion) and if it is too
rough, nothing can be proved (false alarm).  Although the best
abstraction does exist, it is not computable, and so, must be found
experimentally.

We will provide an intuition for the underlying theory, that of
abstract interpretation, and then report on an application to the
proof of absence of runtime errors in the electric flight control
system of commercial planes.  In this project the abstraction has been
tuned manually to get no false alarm, whence a correctness proof,
certainly a world premiere for a program of that size (see the
ASTREE project, http://www.astree.ens.fr/).

We will conclude by grand challenges for static program/specification
analysis the next 5 to 10 years.

Upcoming Events:

volunteers needed!

--Mitch