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

Clc Number:

Fund Project:

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

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 01,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063