微信服务号

微信订阅号

2025年3月25日 20:40 星期二
首页 > 过刊浏览>2018年第29卷第6期 >1544-1565. DOI:10.13328/j.cnki.jos.005463
PDF HTML阅读 XML下载 导出引用 引用提醒
自动合成数组不变式
作者:
作者简介:

李彬(1988-),男,河北邯郸人,博士生,主要研究领域为软件工程,程序分析,程序验证;翟娟(1988-),女,博士,CCF专业会员,主要研究领域为软件工程,程序分析,程序验证,程序合成;汤震浩(1989-),男,博士生,主要研究领域为软件工程,程序分析,程序验证;汤恩义(1982-),男,博士,助理研究员,CCF专业会员,主要研究领域为软件工程,新型软件测试方法与程序分析方法;赵建华(1971-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,软件工程,程序设计语言.

通讯作者:

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

基金项目:

国家自然科学基金（61632015，61561146394）；国家重点研发计划（2016YFB1000802）


Automatic Invariant Synthesis for Array Programs
Author:
Fund Project:

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

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [28]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    提出了基于抽象解释框架自动合成数组程序不变式的方法，它能够分析按照特定顺序访问一维或者多维数组的程序，然后合成不变式.该方法将性质（包括区间全称量词性质和原子性质）集合作为抽象域，通过前向迭代数据流分析合成数组性质.证明了该方法的正确性和收敛性，并通过一些实例展示了该方法的灵活性.开发了一种原型工具，该工具在各种数组程序（包括competition on software verification中的array-examples benchmark）上的实验展示了方法的可行性和有效性.

    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.

    参考文献
    [1] Flanagan C, Qadeer S. Predicate abstraction for software verification. ACM SIGPLAN Notices, 2002,37(1):191-202.[doi:10.1145/565816.503291]
    [2] Lahiri SK, Bryant RE. Indexed predicate discovery for unbounded system verification. In:Alur R, Peled DA, eds. Proc. of the Computer Aided Verification. Berlin:SpringerVerlag, 2004. 135-147.[doi:10.1007/978-3-540-27813-9_11]
    [3] Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Path invariants. ACM SIGPLAN Notices, 2007,42(6):300-309.[doi:10. 1145/1273442.1250769]
    [4] Jhala R, McMillan KL. Array abstractions from proofs. In:Damm W, Hermanns H, eds. Proc. of the Computer Aided Verification. Berlin:Springer-Verlag, 2007. 193-206.[doi:10.1007/978-3-540-73368-3_23]
    [5] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. A static analyzer for large safety-critical software. ACM SIGPLAN Notices, 2003,38(5):196-207.[doi:10.1145/780822.781153]
    [6] Gopan D. Numeric program analysis techniques with applications to array analysis and library summarization[Ph.D. Thesis]. Madison:University of Wisconsin, 2007.
    [7] Gopan D, Reps T, Sagiv M. A framework for numeric analysis of array operations. ACM SIGPLAN Notices, 2005,40(1):338-350.[doi:10.1145/1047659.1040333]
    [8] Halbwachs N, Péron M. Discovering properties about arrays in simple programs. ACM SIGPLAN Notices, 2008,43(6):339-348.[doi:10.1145/1379022.1375623]
    [9] Gulwani S, McCloskey B, Tiwari A. Lifting abstract interpreters to quantified logical domains. ACM SIGPLAN Notices, 2008, 43(1):235-246.[doi:10.1145/1328897.1328468]
    [10] Kam JB, Ullman JD. Monotone data flow analysis frameworks. Acta Informatica, 1977,7(3):305-317.[doi:10.1007/BF00290339]
    [11] Zhao JH, Li XD. Scope logic:An extension to hoare logic for pointers and recursive data structures. In:Liu ZM, ed. Proc. of the Theoretical Aspects of Computing (CICTAC 2013). Shanghai:Springer-Verlag, 2013. 409-426.[doi:10.1007/978-3-642-39718-9_24]
    [12] http://clang.llvm.org/
    [13] De Moura L, Bjrner N. Z3:An efficient smt solver. In:Ramakrishnan CR, Rehof J, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008. 337-340.[doi:10.1007/978-3-540-78800-3_24]
    [14] http://sv-comp.sosy-lab.org/2017/index.php
    [15] Hoare CA. Proof of a program:Find. Communications of the ACM, 1971,14(1):39-45.[doi:10.1145/362452.362489]
    [16] https://github.com/sosy-lab/sv-benchmarks/releases/tag/svcomp17
    [17] Cousot P, Cousot R, Logozzo F. A parametric segmentation functor for fully automatic and scalable array content analysis. ACM SIGPLAN Notices, 2011,46(1):105-118.[doi:10.1145/1925844.1926399]
    [18] Kovács L, Voronkov A. Finding loop invariants for programs over arrays using a theorem prover. In:Chechik M, Wirsing M, eds. Proc. of the Fundamental Approaches to Software Engineering. Berlin:Springer-Verlag, 2009. 470-485.[doi:10.1007/978-3-642-00593-0_33]
    [19] Daniel L, Rodríguez-Carbonell E, Rubio A. SMT-Based array invariant generation. In:Giacobazzi R, Berdine J, Mastroeni I, eds. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin:Springer-Verlag, 2013. 169-188.[doi:10.1007/978-3-642-35873-9_12]
    [20] Francesco A, Ghilardi S, Sharygina N. Decision procedures for flat array properties. In:Ábrahám E, Havelund K, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-averlag, 2014. 15-30.[doi:10.1007/978-3-642-54862-8_2]
    [21] Cordeiro L, Fischer B, Marques-Silva J. SMT-Based bounded model checking for embedded ANSI-C software. IEEE Trans. on Software Engineering, 2012,38(4):957-974.[doi:10.1109/TSE.2011.59]
    [22] Haran A, Carter M, Emmi M, Lal A, Qadeer S, Rakamarić Z. Smack+ Corral:A modular verifier. In:Baier C, Tinelli C, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2015. 451-454.[doi:10.1007/978-3-662-46681-0_42]
    [23] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. Design and implementation of aspecialpurpose static program analyzer for safety-critical real-time embedded software. In:Mogensen TÆ, Schmidt DA, Sudborough IH, eds. Proc. of the Essence of Computation. Berlin:Springer-Verlag, 2002. 85-108.[doi:10.1007/3-540-36377-7_5]
    [24] Gopan D, DiMaio F, Dor N, Reps T, Sagiv M. Numeric domains with summarized dimensions. In:Jensen K, Podelski A, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2004. 512-529.[doi:10.1007/978-3-540-24730-2_38]
    [25] Lahiri SK, Bryant RE. Constructing quantified invariants via predicate abstraction. In:Steffen B, Levi G, eds. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin:Springer-Verlag, 2004. 267-281.[doi:10.1007/978-3-540-24622-0_22]
    [26] Lahiri SK, Bryant RE, Cook B. A symbolic approach to predicate abstraction. In:Hunt WA, Somenzi F, eds. Proc. of the Computer Aided Verification. Berlin:Springer-Verlag, 2003. 141-153.[doi:10.1007/978-3-540-45069-6_15]
    [27] Srivastava S, Gulwani S. Program verification using templates over predicate abstraction. ACM SIGPLAN Notices, 2009,44(6):223-234.[doi:10.1145/1543135.1542501]
    [28] McMillan KL. Quantified invariant generation using an interpolating saturation prover. In:Ramakrishnan CR, Rehof J, eds. Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008. 413-427.[doi:10.1007/978-3-540-78800-3_31]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:3933
  • 下载次数: 4940
  • HTML阅读次数: 2899
  • 引用次数: 0
历史
  • 收稿日期:2017-06-30
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19731573位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号