Extensible Shape Analysis with Invariant Checkers (Xisa)
Bor-Yuh Evan Chang, Xavier Rival and George Necula
National Science Foundation CCR-0326577, National Science Foundation CCF-0524784, National Science Foundation CNS-0509544 and National Science Foundation
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.