Automatic Invariant Synthesis for Array Programs
Author:
Affiliation:

Clc Number:

Fund Project:

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

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This paper proposes a method of using abstract interpretation for discovering properties about array contents in programs which manipulate one-dimensional or multi-dimensional arrays by sequential traversal. The method directly treats invariant properties (including interval universally quantified formulas and atomic formulas) set as abstract domains. It synthesizes invariants by "iterating forward" analysis. This method is sound and converges in finite time. The paper demonstrates the flexibility of the method by some examples. The method has been implemented in a prototype tool. The experiments applying the tool on a variety of array programs (including array-examples benchmark of competition on software verification) demonstrate the feasibility and effectiveness of the approach.

    Reference
    Related
    Cited by
Get Citation

李彬,翟娟,汤震浩,汤恩义,赵建华.自动合成数组不变式.软件学报,2018,29(6):1544-1565

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:June 30,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