The Hob System for Verifying Software Design Properties
Speaker: Patrick Lam , Ph.D. Candidate, CSAIL
Date: December 18 2006
Time: 2:00PM to 3:00PM
Location: 32-D463 Star
Host: Martin Rinard, MIT-CSAIL
Contact: Mary McDavitt, 617-253-9620, mmcdavit@csail.mit.edu
Relevant URL: Abstract:
Abstract: This dissertation introduces novel techniques for verifying
that programs conform to their designs. My Hob system, as described in
this dissertation, allows developers to statically ensure that
implementations preserve certain specified properties. Hob verifies
heap-based properties that can express important aspects of a program's
design. The key insight behind my approach is that Hob can establish
detailed software design properties---properties lie beyond the reach of extant static analysis techniques due to scalability or precision
issues---by focusing the verification task. In particular, the Hob
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, e.g. heap
shape properties. A set-based specification language enables the
different analysis techniques to cooperate in verifying the specified
design properties. My preliminary results show that it is possible to
successfully verify detailed design-level properties of benchmark
applications.
See other events that are part of
See other events happening in December 2006
