Radu Rugina
Cornell University

Practical Shape Analysis


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