Modern programs, particular object-oriented programs, produce large and complex object structures at run time. We lack a good theory of these structures, making it possible to answer important questions such as aliasing (can two reference expressions ever point to the same object?) correctly and efficiently. I will present "object diagrams", a comprehensive theoretical basis for discussing object structures, relying in part on concepts from abstract interpretation. The theory opens the way to sound and efficient alias analysis parameterized by an arbitrary level of precision.

The talk will present a recent implementation of this analysis, and its application to such practical problems as frame analysis (inferring what operations can change) and deadlock analysis in concurrent programming. It will compare the results with those of other approaches to heap analysis (such as sepration logic) and conventional techniques of alias analysis.

Some of the results come from joint work with Sergey Velder (on the theory side) and Victor Rivera (for the implementation of alias analysis).