Static Analysis of Relations between Objects
Viktor Kuncak

Static analysis can discover software errors and prove program properties of interest. Static analysis of relations between objects, such as shape analysis and role analysis, enables the partial verification of programs that manipulate dynamically allocated data structures such as linked lists and trees. Moreover, when objects and relations denote high-level concepts, the analysis can verify design constraints such as cardinality constraints in object models.

I will first present role analysis, which enables the compositional interprocedural verification of movements of objects between data structures. By tracking incoming references of objects and by taking into account data structure invariants, role analysis allows the precise verification of typestate changes in the presence of aliasing. I will next present fundamental decidability and undecidability results arising from problems in role analysis, formalized using the notions of regular graph constraints and boolean shape analysis constraints. These decidability results provide guidance in choosing an appropriate abstraction for the analysis of relations between objects. Finally, I will present role logic, a convenient notation for specifying properties suitable for verification by role analysis. The use of role logic enables role analysis to verify that a program conforms to constraints expressed in UML object models or entity-relationship diagrams, leveraging commonly used software documentation as a source of verifiable program specifications.

Back to the Programming Systems Graduate Zeminar.


Last updated: Tue Feb 10 16:34:05 EST 2004