Node-Set Analysis for Linked Recursive Data Structures

The technique presented in this paper concerns the problem of how to automatically obtaining the specification of the resulting set of reachable nodes, after destructive operations over the data structure. Our work has two main contributions. First, we represent the node sets by expressions at pre-states, which facilitates the process of proving complex formulas efficiently. Second, we propose an improved version of the fold/unfold technique, which handles more general cases. Our approach is based on the observation that structure-update statements manipulate recursive data structures in a slice-and-splice way: the original data structures are sliced into several disjoint segments and these segments are further spliced into new data structures. Case studies on typical data structures show that our approach is effective and practical.