[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, September 18, 2002
206 Egan  Hall, Northeastern University
    (building 44 on http://www.campusmap.neu.edu/)
9:00-11:00

Cormac Flanagan 
(SRC, DEC/Compaq/HP)

Program Checking = Logic + Lambda

Ensuring the correctness and reliability of a software system is a
challenging problem. Documenting correctness properties that the
system should obey is straightforward. For example, it should not
dereference dangling pointers or read from unopened files. However,
verifying that the system actually satisfies these properties is much
harder.

Automatic theorem proving provides a promising approach for verifying
that a code fragment satisfies its correctness properties for all
possible input values. However, existing fully-automatic theorem provers are
unable to reason directly about code that uses iteration or recursion,
and instead require the programmer to help by supplying loop
invariants and procedure specifications. The burden of providing these
annotations has so far limited the cost-effectiveness of such checking
tools.

This talk presents a novel, annotation-free approach to program
checking. Our approach is based on an extended logic that provides
explicit support for iteration and recursion.  Although the
satisfiability of queries in this logic is undecidable in general, we
present an efficient semi-algorithm based on a combination of lazy
abstraction, counter-example driven abstraction refinement, and
explicating, proof-generating decision procedures for specific theories
such as linear arithmetic.

The problem of deciding if a software system satisfies its correctness
properties can be then expressed as a satisfiability query in this
logic, without burdening the programmer with supplying loop invariants
and procedure specifications.



Upcoming presentations:

We will resume our regular meetings in a couple of weeks.  These will
most likely be on Wednesday mornings as in the past.  We will devote a
few minutes on the 18th to organizing this.  If you can't come on the
18th, but would like to influence our choice of a regular meeting
time, please email me beforehand.

--Mitch