自动分析递归数据结构的归纳性质

本文提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为三个主要部分.首先，它将递归数据结构的归纳性质分为两个主要类别，并提出对应的处理模式，从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次，提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据结构首先被分割为若干个互不相交的片段，然后这些片段以新的方式重新拼接在一起，形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来，从而为后面的分析过程所使用.最后，提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明我们的分析框架可以有效地分析递归数据结构的归纳性质，并生成对程序证明过程有用的断言.

Automatically Analyzing Inductive Properties for Recursive Data Structures

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