Automatic Invariant Synthesis for Array Programs
Author:
Affiliation:

Fund Project:

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

  • Article
  • | |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • | |
  • 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
    Comments
    Comments
    分享到微博
    Submit
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
You are the first2033165Visitors
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