微信服务号

微信订阅号

2025-5-2- 4
Home > Archive>Volume 28, Issue 5, 2017 >1051-1069. DOI:10.13328/j.cnki.jos.005211
PDF HTML XML Export Cite reminder
Automatic Approach of Generating Summaries for Common Loops and Its Application
Author:
Affiliation:

Fund Project:

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

  • Article
    • | |
  • Metrics
    • |
  • Reference [54]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    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.

    Reference
    [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.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:4209
  • PDF: 6241
  • HTML: 3734
  • Cited by: 0
History
  • Received:July 15,2016
  • Revised:September 25,2016
  • Online: January 22,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2041544Visitors
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