Abstract:This paper proposes a framework facilitating the automatic analysis on inductive properties for recursive data structures. This work has three main parts. First, the analysis of heap-manipulating programs is simplified by classifying inductive properties of recursive data structures into two classifications, each of them is handled with observed patterns. Second, a slicing and splicing technique, in which data structures are first sliced into several parts and these parts are further spliced into new data structures, is proposed to track and specify how data structures are manipulated by programs. The key idea of this technique is to preserve the properties of original data structures, which can be used by further analysis. Third, a calling context sensitive interprocedural analysis is presented for computing program summaries. A case study and experimental results show that the proposed analysis framework can effectively analyze inductive properties for recursive data structures, resulting in assertions that are helpful in program verification.