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.
|