[Colloq] Philippe Meunier's dissertation defense

[Diane Keys]

College of Computer and Information Science

PhD Dissertation Defense:
Philippe Meunier

Title:
Modular Set-based Analysis from Contracts

Monday, May 15th at 1:00 p.m.

366 WVH


Abstract:

Detecting bugs before releasing software is a major goal of software
engineering.  While a rigorous software development process and
systematic testing help, only formal methods can guarantee the absence
of bugs, or at least the absence of some classes of bugs.  From sound
type systems to theorem provers, such formal systems have been
available for a long time, but the adoption of these advanced systems
has been slow, due to both their inherent complexity as well as their
sometimes poor running times.

In this dissertation we explain how to make a value-flow analysis
(0-CFA) modular, using runtime monitoring contracts as if they were
static module interface specifications.  The analysis statically
computes a conservative approximation of the values and errors that
each expression in a program might produce at runtime.  Using a
graphical static debugger based on this analysis, programmers can then
analyze the program modules they are working on even when the source
code of the whole program is not available, and interactively view the
flows of values in the modules to easily trace the sources of bugs.

Committee members: Matthias Felleisen, Mitchell Wand, Karl Lieberherr,
Cormac Flanagan, Robert Findler.