主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
汤震浩,李彬,翟娟,赵建华.自动分析递归数据结构的归纳性质.软件学报,2018,29(6):1527-1543
自动分析递归数据结构的归纳性质
Automatically Analyzing Inductive Properties for Recursive Data Structures
投稿时间:2017-07-01  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005467
中文关键词:  霍尔式程序证明  程序分析  递归数据结构  归纳性质  过程间分析
英文关键词:Hoare-Style program verification  program analysis  recursive data structures  inductive properties  interprocedural analysis
基金项目:国家重点研发计划(2016YFB1000802);国家自然科学基金(61632015,61561146394)
作者单位E-mail
汤震浩 南京大学 计算机科学与技术系, 江苏 南京 210023
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
 
李彬 南京大学 计算机科学与技术系, 江苏 南京 210023
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
 
翟娟 南京大学 计算机科学与技术系, 江苏 南京 210023
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
 
赵建华 南京大学 计算机科学与技术系, 江苏 南京 210023
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
zhaojh@nju.edu.cn 
摘要点击次数: 718
全文下载次数: 543
中文摘要:
      提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先,它将递归数据结构的归纳性质分为两个主要类别,并提出对应的处理模式,从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次,提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的:递归数据结构首先被分割为若干个互不相交的片段,然后,这些片段以新的方式重新拼接在一起,形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来,从而为后面的分析过程所使用.最后,提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明:分析框架可以有效地分析递归数据结构的归纳性质,并生成对程序证明过程有用的断言.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利