Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences


UC Berkeley


2008 Research Summary

Extensible Shape Analysis with Invariant Checkers

View Current Project Information

Bor-Yuh Evan Chang, Xavier Rival and George Necula

Shape analyses are unique in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To do so, they rely on specialized data structure descriptions to build and decompose summaries of memory regions. Unfortunately, existing approaches suffer from usability and scalability issues that make them impractical to apply broadly. Typically, they either are insufficiently extensible or require low-level, expert interaction. Instead, our project focuses first on practicality by designing an extensible shape analysis based around high-level, program developer-oriented specifications. In particular, we observe that data structure checking code (e.g., used in testing or dynamic analysis) provides shape information that can also be used effectively in static analysis.

B.-Y. E. Chang, X. Rival, and G. C. Necula, "Shape Analysis with Structural Invariant Checkers," Static Analysis Symposium (SAS), 2007.
B.-Y. E. Chang and X. Rival, "Relational Inductive Shape Analysis," Symposium on Principles of Programming Languages (POPL), 2008.