Mike Ernst's talk at 1pm in 2310

["Rastislav Bodik" <bodik@xxxxxxxxxxx>]

Hi all,

Please take an hour off from your busy finals week and attend the talk at
1pm, in 2310.

Ras

	Dynamically Detecting Likely Program Invariants

	Mike Ernst, MIT

Explicitly stated program invariants can help programmers by characterizing
certain aspects of program execution and identifying program properties
that must be preserved when modifying code.  In practice, these invariants
are usually absent from code.  An alternative to expecting programmers to
annotate code with invariants is to automatically infer invariants from the
program itself.

This talk describes dynamic techniques for discovering invariants from
execution traces; the essential idea is to look for patterns in and
relationships among variable values over a set of executions.  An
implementation has indicated that the approach is both effective --
successfully rediscovering formal specifications -- and useful --
discovering invariants that assisted a software evolution task.

A naive implementation of dynamic invariant inference suffers both from
excessive runtime and also from reporting irrelevant invariants and failing
to report relevant ones.  I will discuss several improvements that together
make the system usable:  statistical confidence measures, eliminating
unused polymorphism, suppressing redundant and coincidentally true
properties, and limiting which variables are compared to one another.  I
will also show how to extend dynamic invariant inference to
pointer-directed data structures, which requires traversal of data
structures and discovery of conditional rather than universally true
invariants.

This is joint work with Jake Cockrell, Adam Czeisler, Bill Griswold, Josh
Kataoka, Jeremy Nimmer, and David Notkin.