-
题名自动分析递归数据结构的归纳性质
被引量：2
- 1
-
-
作者
汤震浩
李彬
翟娟
赵建华
-
机构
南京大学计算机科学与技术系
计算机软件新技术国家重点实验室(南京大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2018年第6期1527-1543,共17页
-
基金
国家重点研发计划(2016YFB1000802)
国家自然科学基金(61632015
61561146394)~~
-
文摘
提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先,它将递归数据结构的归纳性质分为两个主要类别,并提出对应的处理模式,从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次,提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的:递归数据结构首先被分割为若干个互不相交的片段,然后,这些片段以新的方式重新拼接在一起,形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来,从而为后面的分析过程所使用.最后,提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明:分析框架可以有效地分析递归数据结构的归纳性质,并生成对程序证明过程有用的断言.
-
关键词
霍尔式程序证明
程序分析
递归数据结构
归纳性质
过程间分析
-
Keywords
Hoare-Style program verification
program analysis
recursive data structures
inductive properties
interprocedural analysis
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
