Radu
Rugina
Cornell University
Abstract:
Shape analyses are
aimed at extracting invariants that describe the
"shapes" of
heap-allocated recursive data structures. Although existing
shape analyses
have been successful at verifying complex heap
manipulations,
they have had limited success at being practical for
larger programs.
In this talk I will
present practical approaches to heap analysis and their application to error
detection, program verification, and compiler
transformations.
First, I will present a reference counting shape
analysis where
the compiler uses local reasoning about individual heap
cells, instead
of global reasoning about the entire heap. Second, I will present a heap analysis by
contradiction, where the analysis checks the
absence of heap
errors by disproving their presence. These techniques are both sufficiently
precise to accurately analyze a large class of
heap
manipulation algorithms, and sufficiently lightweight to scale to larger programs.
Host: Bob Harper
Appointments:
April Foster <aprilf@cs.cmu.edu>
Friday, March 2, 2007
3:30 p.m.
Wean
Hall 8220
Principles
of Programming Seminars