SATC: Shape Analysis with Tracked Cells

        A scalable approach to heap analysis

This project explores novel heap abstractions and analyses that use local reasoning about single heap cells. Our approach uses local heap abstractions to describe the state of single heap cells, instead of global heap abstractions (such as shape graphs) that describe entire heaps. This makes it possible to build scalable, but accurate intra-procedural and inter-procedural heap analyses. Our shape analysis implementations have been successfully applied to programs of tens of thousands of lines of C and Java code. We investigate the application of this technology to problems that require reasoning about memory and aliases, including memory error detection, memory management, and verification of safety properties properties.


Download shape-suif.tgz, a heap error detection tool for C programs that uses shape analysis with tracked cells. This is an implementation in the SUIF1 compiler infrastructure. An implementation of shape analysis for C in the Crystal framework is currently under development.


Related projects

Current and Past Members: