Monday, September 11, 2006
11:00 AM
CSB 209
Radu Rugina
Static Analysis of Dynamic Heap Structures
Dynamic allocation and destructive heap updates are fundamental language constructs that allow programmers to implement complex, efficient linked data structures. However, their flexibility makes it difficult for compilers and program analyzers to statically reason about the correct manipulation of such structures.

In this talk I will discuss novel program analysis techniques for inter-procedural and recursive heap manipulations, and the application of these techniques to error detection, program verification, and compiler transformations. First, I will present a reference counting heap 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.

Bio: Radu Rugina is an Assistant Professor in the Department of Computer Science at Cornell University. He received his Ph.D. from the University of California, Santa Barbara in 2002. Between 1997 and 2001 he was a visiting scholar at the MIT Laboratory for Computer Science. Radu Rugina's reaseach interests are in static analysis and compilation techniques for program understanding, verification, and transformation.