自动分析递归数据结构的归纳性质
作者:
作者单位:

作者简介:

汤震浩(1989-),男,江苏南通人,博士生,主要研究领域为软件工程,程序分析,程序验证;李彬(1988-),男,博士生,主要研究领域为软件工程,程序分析,程序验证;翟娟(1988-),女,博士,CCF专业会员,主要研究领域为软件工程,程序分析,程序验证,程序合成;赵建华(1971-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,软件工程,程序设计语言.

通讯作者:

赵建华,E-mail:zhaojh@nju.edu.cn

中图分类号:

基金项目:

国家重点研发计划(2016YFB1000802);国家自然科学基金(61632015,61561146394)


Automatically Analyzing Inductive Properties for Recursive Data Structures
Author:
Affiliation:

Fund Project:

National Key Research and Development Program of China (2016YFB1000802); National Natural Science Foundation of China (61632015, 61561146394)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

汤震浩,李彬,翟娟,赵建华.自动分析递归数据结构的归纳性质.软件学报,2018,29(6):1527-1543

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2017-07-01
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号