微信服务号

微信订阅号

2025年8月7日 20:46 星期四
首页 > 过刊浏览>2017年第28卷第5期 >1051-1069. DOI:10.13328/j.cnki.jos.005211
PDF HTML阅读 XML下载 导出引用 引用提醒
常用循环摘要的自动生成方法及其应用
作者:
基金项目:

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


Automatic Approach of Generating Summaries for Common Loops and Its Application
Author:
Fund Project:

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

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

    采用形式化方法证明软件的正确性，是保障软件可靠性的有效方法.而对循环语句的分析与验证，是形式化证明中的关键，对循环语句的处理一直是程序分析与验证中的一个难点问题.提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果，并将该执行效果定义为循环摘要.同时，提出一种自动生成循环摘要的方法，可以为操作常用数据结构的循环自动生成循环摘要，包含嵌套循环.此外，基于循环摘要，可以自动生成循环语句的规约，包括循环不变式、循环的前置条件以及循环的后置条件.已经实现了自动生成循环摘要以及循环规约的方法，并将它们集成到验证工具Accumulator中.实验结果表明，该方法可以有效地生成循环摘要，并生成多种类型的规约，从而辅助软件程序的形式化证明，提高验证的自动化程度和效率，减轻验证人员的负担.

    Abstract:

    Formal verification is an effective method to guarantee software reliability by proving the correctness of a program. Analyzing and verifying loops which are important and frequently-used statements is not only vital for formal verification, but also a hot topic in the research area of software development. This paper proposes using memories modified by a loop and new values stored in these memories after executing the loop to describe the execution effect of the loop. Such execution effect is defined as loop summary. In addition, this paper proposes an approach to automatically synthesize loop summaries for loops manipulating commonly-used data structures, including nested loops. Based on loop summaries, specifications can be generated automatically, including loop invariants, preconditions and post-conditions of loops. The proposed approach is implemented and integrated into the code-verification tool Accumulator. The approach is also evaluated with a variety of programs, and the results show that it is able to generate loop summaries and different kinds of specifications, therefore helping to ease the verification task by reducing the burden for programmers and improving the automatic level and efficiency.

    参考文献
    [1] Floyd RW. Assigning meaning to programs. In: Proc. of the Symp. in Applied Mathematics. 1967. 19-32.
    [2] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580. [doi: 10.1145/ 363235.363259]
    [3] Dijkstra EW. A Discipline of Programming. Prentice Hall, Inc., 1976.
    [4] Furia CA, Meyer B. Inferring loop invariants using postconditions. In: Proc. of the Fields of Logic and Computation. 2010. 277-300. [doi: 10.1007/978-3-642-15025-8_15]
    [5] Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Chen X. The daikon system for dynamic detection of likely invariants. Science of Computer Programming, 2007,69(1-3):35-45. [doi: 10.1016/j.scico.2007.01.015]
    [6] Tsitovich A, Sharygina N, Wintersteiger CM, Kroening D. Loop summarization and termination analysis. In: Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. 2011. 81-95. [doi: 10.1007/978-3-642-19835-9_9]
    [7] Papanicolau G, Keller JB. Automatic partial loop summarization in dynamic test generation. In: Proc. of the Int'l Symp. on Software Testing and Analysis. Toronto, 2011. 23-33. [doi: 10.1145/2001420.2001424]
    [8] Kroening D, Sharygina N, Tonetta S, Tsitovich A, Wintersteiger CM. Loop summarization using abstract transformers. In: Proc. of the Int'l Symp. on Automated Technology for Verification and Analysis. Seoul, 2008. 111-125. [doi: 10.1007/978-3-540-88387-6_ 10]
    [9] Chawdhary A, Cook B, Gulwani S, Sagiv M, Yang H. Ranking abstractions. In: Proc. of the European Conf. on Theory & Practice of Software. 2008. 148-162. [doi: 10.1007/978-3-540-78739-6_13]
    [10] https://memcached.org/
    [11] https://httpd.apache.org/
    [12] https://nginx.org/en/
    [13] Zhao JH, Li XD. Scope logic: An extension to Hoare logic for pointersand recursive data structures. In: Proc. of the Theoretical Aspects of Computing. 2013. 409-426. [doi: 10.1007/978-3-642-39718-9_24]
    [14] http://seg.nju.edu.cn/toolweb/index.html
    [15] De Moura L, Bjorner N. Z3: An efficient SMT solver. In: Proc. of the Int'l Conf. of Tools and Algorithms for the Construction and Analysis of Systems. 2008. 337-340. [doi: 10.1007/978-3-540-78800-3_24]
    [16] Nie CJ, Liu HF, Su PR, Feng DG. A loop summarization method for dynamic binary program analysis. Acta Electronica Sinica, 2014,42(6):1110-1117 (in Chinese with English abstract).
    [17] Kroening D, Sharygina N, Tonetta S, Tsitovich A，Wintersteiger CM. Loop summarization using state and transition invariants. Formal Methods in System Design, 2013,42(3):221-261. [doi: 10.1007/s10703-012-0176-y]
    [18] Reps TW, Sagiv S, Yorsh G. Symbolic implementation of the best transformer. In: Proc. of the Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. 2004. 252-266. [doi: 10.1007/978-3-540-24622-0_21]
    [19] Bozga M, Iosif R, Konečný F. Deciding conditional termination. In: Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2014. 252-266. [doi: 10.1007/978-3-642-28756-5_18]
    [20] Cook B, Gulwani S, Lev-Ami T, Rybalchenko A, Sagiv M. Proving conditional termination. In: Proc. of the Int'l Conf. of Computer Aided Verification. Springer-Verlag, 2008. 328-340. [doi: 10.1007/978-3-540-70545-1_32]
    [21] Moy Y. Sufficient preconditions for modular assertion checking. In: Proc. of the Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, 2008. 188-202. [doi: 10.1007/978-3-540-78163-9_18]
    [22] Seghir MN, Kroening D. Counterexample-Guided precondition inference. In: Proc. of the Programming Languages and Systems. Springer-Verlag, 2013. 451-471. [doi: 10.1007/978-3-642-37036-6_25]
    [23] Lopes NP, Monteiro J. Weakest precondition synthesis for compiler optimizations. In: Proc. of the Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, 2014. 203-221. [doi: 10.1007/978-3-642-54013-4_12]
    [24] Flanagan C, Saxe JB. Avoiding exponential explosion: Generating compact verification conditions. In: Proc. of the Symp. on Principles of Programming Language. ACM Press, 2001. 193-205. [doi: 10.1145/360204.360220]
    [25] Leino KRM. Efficient weakest preconditions. Information Processing Letters, 2005,93(6):281-288. [doi: 10.1016/j.ipl.2004.10.0 15]
    [26] Jager I, Brumley D. Efficient directionless weakest preconditions. Technical Report, CMU-CyLab-10-002, CyLab, Carnegie Mellon University, 2010.
    [27] Mraihi O, Ghardallou W, Louhichi A, Jilani LL, Bsaies K, Mili A. Computing preconditions and postconditions of while loops. In: Proc. of the Theoretical Aspects of Computing. Springer-Verlag, 2011. 173-193. [doi: 10.1007/978-3-642-23283-1_13]
    [28] Barnett M, Leino KRM. Weakest-Precondition of unstructured programs. In: Proc. of the ACM SIGSOFT Software Engineering Notes. ACM Press, 2005. 82-87. [doi: 10.1145/1108792.1108813]
    [29] Louhichi A, Mraihi O, Jilani LL, Mili A. Invariant assertions, invariant relations, and invariant functions. Innovations in Systems and Software Engineering, 2012,8(3):195-212.
    [30] Zhai J, Wang H, Zhao JH. Assertion-Directed precondition synthesis for loops over data structures. In: Proc. of the Dependable Software Engineering: Theories, Tools, and Applications. 2015. 258-274. [doi: 10.1007/978-3-319-25942-0_17]
    [31] 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/1040305.1040333]
    [32] Mine A. The octagon abstract domain. Higher-Order and Symbolic Computation, 2006,19(1):31-100. [doi: 10.1007/s10990-006-86 09-1]
    [33] Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. of the 5th ACM SIGACTSIGPLAN Symp. on Principles of Programming Languages. ACM Press, 1978. 84-96. [doi: 10.1145/512760.512770]
    [34] Rodríguez-Carbonell E, Kapur D. An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi R, ed. Proc. of the Int'l Static Analysis Symp. (SAS 2004). LNCS 3148, Berlin, Heidelberg: Springer-Verlag, 2004. 280-295. [doi: 10.1007/978-3-540-27864-1_21]
    [35] Xing JY, Li MJ, Li ZJ. CILinear: An automated generation tool of linear invariant. Computer Science, 2010,37(12):91-95 (in Chinese with English abstract).
    [36] Flanagan C, Qadeer S. Predicate abstraction for software verification. ACM SIGPLAN Notices, 2002,37(1):191-202. [doi: 10.114 5/565816.503291]
    [37] Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R. Extended static checking for Java. In: Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2002. 234-245. [doi: 10.1145/512529.512558]
    [38] Colon MA, Sankaranarayanan S, Sipma HB. Linear invariant generation using non-linear constraint solving. In: Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2003. 420-432. [doi: 10.1007/978-3-540-45069-6_39]
    [39] Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Invariant synthesis for combined theories. In: Proc. of the Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, 2007. 378-394. [doi: 10.1007/978-3-540-69738-1_27]
    [40] Bi ZQ, Zeng ZB, Guo YH. Automatic generation of non-linear loop invariants. Jounal of Computer Applications, 2008,28(7):1854-　1857 (in Chinese with English abstract).
    [41] Liu ZH, Zeng QK. An adaptive loop invariant generation approach. Computer Engineering, 2013,39(6):76-81 (in Chinese with English abstract).
    [42] Janota M. Assertion-Based loop invariant generation. In: Proc. of the RISC-Linz. 2007.
    [43] Zhai J, Wang H, Zhao JH. Post-Condition-Directed invariant inference for loops over data structures. In: Proc. of the Software Security and Reliability-Companion. IEEE, 2014. 204-212. [doi: 10.1109/SERE-C.2014.40]
    [44] Ma ZG, Wang CM. An approach of creating loop invariant based on gene expression programming. Computer and Digital Engineering, 2009,37(7):7-10 (in Chinese with English abstract).
    [45] Liu G, Chen YY, Zhang ZT. Automatic inference of loop-invariant shape graphs. Electronic Technology, 2011,38(8):4-6 (in Chinese with English abstract).
    [46] Liang HJ, Zhang Y, Chen YY, Li ZP. A shape system and loop invariant inference. https://www.researchgate.net/publication/22864 6559_A_Shape_System_and_Loop_Invariant_Inference
    [47] Magill S, Nanevski A, Lee CEP. Inferring invariants in separation logic for imperative list-processing programs. In: Proc. of the SPACE Workshop. 2006.
    附中文参考文献:
    [16] 聂楚江,刘海峰,苏璞睿,冯登国.一种面向程序动态分析的循环摘要生成方法.电子学报,2014,42(6):1110-1117.
    [35] 邢建英,李梦君,李舟军.CILinear:一个线性不变式自动构造工具.计算机科学,2010,37(12):91-95.
    [40] 毕忠勤,曾振柄,郭远华.非线性循环不变式的自动生成.计算机应用,2008,28(7):1854-1857.
    [41] 刘自恒,曾庆凯.一种自适应的循环不变式生成方法.计算机工程,2013,39(6):76-81.
    [44] 马竹根,王灿明.利用基因表达式编程自动生成循环不变式.计算机与数字工程,2009,37(7):7-10.
    [45] 刘刚,陈意云,张志天.循环不变形状图的自动推断.电子技术,2011,38(8):4-6.
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

翟娟,汤震浩,李彬,赵建华,李宣东.常用循环摘要的自动生成方法及其应用.软件学报,2017,28(5):1051-1069

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

京公网安备 11040202500063号