微信服务号

微信订阅号

2025-4-24- 14
Home > Archive>Volume 29, Issue 6, 2018 >1527-1543. DOI:10.13328/j.cnki.jos.005467
PDF HTML XML Export Cite reminder
Automatically Analyzing Inductive Properties for Recursive Data Structures
Author:
Affiliation:

Fund Project:

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

  • Article
    • | |
  • Metrics
    • |
  • Reference [29]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    This paper proposes a framework facilitating the automatic analysis on inductive properties for recursive data structures. This work has three main parts. First, the analysis of heap-manipulating programs is simplified by classifying inductive properties of recursive data structures into two classifications, each of them is handled with observed patterns. Second, a slicing and splicing technique, in which data structures are first sliced into several parts and these parts are further spliced into new data structures, is proposed to track and specify how data structures are manipulated by programs. The key idea of this technique is to preserve the properties of original data structures, which can be used by further analysis. Third, a calling context sensitive interprocedural analysis is presented for computing program summaries. A case study and experimental results show that the proposed analysis framework can effectively analyze inductive properties for recursive data structures, resulting in assertions that are helpful in program verification.

    Reference
    [1] Zhao J, Li X. Scope logic:An extension to hoare logic for pointers and recursive data structures. In:Proc. of the Theoretical Aspects of Computing (ICTAC 2013). Berlin, Heidelberg:Springer-Verlag, 2013. 409-426.[doi:10.1007/978-3-642-39718-9_24]
    [2] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science. IEEE, 2002. 55-74.[doi:10.1109/LICS.2002.1029817]
    [3] Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Trans. on Programming Languages and Systems (TOPLAS), 2002,24(3):217-298.[doi:10.1145/514188.514190]
    [4] Deutsch A. Interprocedural may-alias analysis for pointers:Beyond k-limiting. ACM SIGPLAN Notices, 1994,29(6):230-241.[doi:10.1145/773473.178263]
    [5] Kreiker J, Seidl H, Vojdani V. Shape analysis of low-level C with overlapping structures. In:Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2010. 214-230.[doi:10.1007/978-3-642-11319-2_17]
    [6] Berdine J, Calcagno C, Cook B, et al. Shape analysis for composite data structures. In:Proc. of the Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2007. 178-192.[doi:10.1007/978-3-540-73368-3_22]
    [7] Holik L, Lengal O, Rogalewicz A, et al. Fully automated shape analysis based on forest automata. In:Proc. of the Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2013. 740-755.[doi:10.1007/978-3-642-39799-8_52]
    [8] Cousot P, Cousot R. Abstract interpretation:A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In:Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM Press, 1977. 238-252.[doi:10.1145/512950.512973]
    [9] Bouajjani A, Dragoi C, Enea C, et al. Abstract domains for automated reasoning about list-manipulating programs with infinite data. In:Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2012. 1-22.[doi:10.1007/978-3-642-27940-9_1]
    [10] Berdine J, Calcagno C, O'hearn PW. Symbolic execution with separation logic. In:Proc. of the Programming Languages and Systems. Berlin, Heidelberg:Springer-Verlag, 2005. 52-68.[doi:10.1007/11575467_5]
    [11] Pek E, Qiu X, Madhusudan P. Natural proofs for data structure manipulation in C using separation logic. In:Proc. of the 35th ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM Press, 2014. 46.[doi:10.1145/2594291.2594325]
    [12] Qiu X, Garg P, Stefanescu A, et al. Natural proofs for structure, data, and separation. ACM SIGPLAN Notices, 2013,48(6):231-242.[doi:10.1145/2491956.2462169]
    [13] Chin WN, David C, Nguyen HH, et al. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, 2012,77(9):1006-1036.[doi:10.1016/j.scico.2010.07.004]
    [14] Lee O, Yang H, Yi K. Automatic verification of pointer programs using grammar-based shape analysis. In:Proc. of the Programming Languages and Systems. Berlin, Heidelberg:Springer-Verlag, 2005. 124-140.[doi:10.1007/978-3-540-31987-0_10]
    [15] de Boer F, Bonsangue M, Rot J. Automated verification of recursive programs with pointers. In:Proc. of the Automated Reasoning. Berlin, Heidelberg:Springer-Verlag, 2012. 149-163.[doi:10.1007/978-3-642-31365-3_14]
    [16] Zee K, Kuncak V, Rinard M. Full functional verification of linked data structures. ACM SIGPLAN Notices, 2008,43(6):349-361.[doi:10.1145/1375581.1375624]
    [17] Itzhaky S, Banerjee A, Immerman N, Lahav O, Nanevski A, Sagiv M. Modular reasoning about heap paths via effectively propositional formulas. In:Proc. of the 41st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM Press, 2014. 385-396.[doi:10.1145/2535838.2535854]
    [18] De Moura L, Bjørner N. Z3:An efficient SMT solver. In:Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2008. 337-340.[doi:10.1007/978-3-540-78800-3_24]
    [19] Zhang X, Mangal R, Naik M, Yang H. Hybrid top-down and bottom-up interprocedural analysis. ACM SIGPLAN Notices, 2014, 49(6):249-258.[doi:10.1145/2594291.2594328]
    [20] Nystrom E, Kim HS, Hwu WM. Bottom-Up and top-down context-sensitive summary-based pointer analysis. In:Proc. of the Static Analysis. 2004. 165-180.[doi:10.1007/978-3-540-27864-1_14]
    [21] Itzhaky S, Bjørner N, Reps TW, Sagiv M, Thakur AV. Property-Directed shape analysis. In:Proc. of the CAV. 2014. 35-51.[doi:10.1007/978-3-319-08867-9_3]
    [22] Rinetzky N, Bauer J, Reps T, Sagiv M, Wilhelm R. A semantics for procedure local heaps and its abstractions. ACM SIGPLAN Notices, 2005,40(1):296-309.[doi:10.1145/1047659.1040330]
    [23] Rinetzky N, Sagiv M, Yahav E. Interprocedural shape analysis for cutpoint-free programs. In:Proc. of the SAS. 2005. 284-302.[doi:10.1007/11547662_20]
    [24] Hoare CA. An axiomatic basis for computer programming. Communications of the ACM, 1969,12(10):576-580.[doi:10.1145/1562764.1562779]
    [25] Hoare T. The verifying compiler:A grand challenge for computing research. Journal of the ACM (JACM), 2003,50(1):63-69.[doi:10.1007/978-3-540-45213-3_4]
    [26] Seo S, Yang H, Yi K. Automatic construction of Hoare proofs from abstract interpretation results. In:Proc. of the Programming Languages and Systems. 2003. 230-245.[doi:10.1007/978-3-540-40018-9_16]
    [27] Dijkstra EW. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975,18(8):453-457.[doi:10.1007/978-1-4612-6315-9_14]
    [28] Tang Z, Wang H, Li B, Zhai J, Zhao JH, Li X. Node-Set analysis for linked recursive data structures. In:Proc. of the 2015 IEEE Int'l Conf. on Software Quality, Reliability and Security (QRS). IEEE, 2015. 59-64.[doi:10.1109/QRS.2015.19]
    [29] Kjolstad F, Dig D, Acevedo G, Snir M. Transformation for class immutability. In:Proc. of the 33rd Int'l Conf. on Software Engineering. ACM Press, 2011. 61-70.[doi:10.1145/1985793.1985803]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

汤震浩,李彬,翟娟,赵建华.自动分析递归数据结构的归纳性质.软件学报,2018,29(6):1527-1543

Copy
Share
Article Metrics
  • Abstract:3592
  • PDF: 6434
  • HTML: 3063
  • Cited by: 0
History
  • Received:July 01,2017
  • Revised:September 01,2017
  • Adopted:November 06,2017
  • Online: December 28,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038072Visitors
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