[PRL] [MIT Thesis Defense] The Hob System for Verifying Data Structure Consistency Properties

[Mitchell Wand]

From: CSAIL Event Calendar <eventcalendar at csail.mit.edu>
To: seminars at csail.mit.edu
Date: Mon, 13 Nov 2006 15:31:42 -0500
Subject: TALK:Thursday 11-30-06 Patrick Lam, Thesis Defense - The Hob
System for V

The Hob System for Verifying Data Structure Consistency Properties
Speaker: Patrick Lam
Speaker Affiliation: Ph.D. Candidate, CSAIL
Host: Martin Rinard
Host Affiliation: MIT-CSAIL

Date: 11-30-2006
Time: 1:00 PM - 3:00 PM
Refreshments: 12:45 PM
Location: 32-G449 Patil/Kiva Conference Room

Abstract:

This dissertation explores techniques for verifying that programs
conform to their designs.  My thesis is that the Hob system described in
this dissertation will allow developers to ensure that data structure
consistency properties hold in all executions of a program; such
properties can express important aspects of the program's design.  The
key insight behind our approach is that we can establish detailed data
structure consistency properties---properties that are beyond the
reach of extant static analysis techniques---by focussing the
verification task.  In particular, our approach applies scalable
static analysis techniques to the majority of the modules of a program
and very precise, unscalable, static analysis or automated theorem
proving techniques to certain specific modules of that program: those
that require the precision that such analyses can deliver.  The use of
assume/guarantee reasoning allows the analysis engine to harness the
strengths of both scalable and precise static analysis techniques to
analyze large programs (which would otherwise require scalable,
imprecise analyses) with sufficient precision to establish detailed
data structure consistency properties, \emph{e.g.}  heap shape
properties.  Our preliminary results show that it is possible to
successfully verify extremely detailed consistency properties of
benchmark applications.