{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:48:59Z","timestamp":1694634539672},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,11,5]],"date-time":"2008-11-05T00:00:00Z","timestamp":1225843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s11704-008-0033-8","type":"journal-article","created":{"date-parts":[[2008,11,5]],"date-time":"2008-11-05T06:41:57Z","timestamp":1225867317000},"page":"380-397","source":"Crossref","is-referenced-by-count":0,"title":["Automated verification of pointer programs in pointer logic"],"prefix":"10.1007","volume":"2","author":[{"given":"Zhifang","family":"Wang","sequence":"first","affiliation":[]},{"given":"Yiyun","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Zhenming","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Baojian","family":"Hua","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,11,5]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Proceedings of the 15th International Workshop on Computer Science Logic","author":"P. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn P, Reynolds J, Yang H. Local reasoning about programs that alter data structures. In: Proceedings of the 15th International Workshop on Computer Science Logic. London: Springer, 2001, 1\u201319"},{"key":"33_CR2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science","author":"J. Reynolds","year":"2002","unstructured":"Reynolds J. Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington: IEEE Computer Society, 2002, 55\u201374"},{"key":"33_CR3","unstructured":"Jonkers H B M. Abstract storage structures. In: de Bakker, van. Vllet, eds. Algorithmic Languages. 1981, 321\u2013343"},{"key":"33_CR4","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/ICCL.1992.185463","volume-title":"Proceedings of the 1992 International Conference on Computer Languages","author":"A. Deutsch","year":"1992","unstructured":"Deutsch A. A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations. In: Proceedings of the 1992 International Conference on Computer Languages. California: IEEE Computer Society, 1992, 2\u201313"},{"issue":"2","key":"33_CR5","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/S0167-6423(99)00012-X","volume":"35","author":"A. Venet","year":"1999","unstructured":"Venet A. Automatic analysis of pointer aliasing for untyped programs. Science of Computer Programming. 1999, 35(2):223\u2013248","journal-title":"Science of Computer Programming"},{"key":"33_CR6","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1145\/777388.777395","volume-title":"Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation","author":"M. Bozga","year":"2003","unstructured":"Bozga M, Iosif R, Laknech Y. Storeless semantics and alias logic. In: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation. New York: ACM Press, 2003, 55\u201365"},{"key":"33_CR7","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/1040305.1040330","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"N. Rinetzky","year":"2005","unstructured":"Rinetzky N, Bauer J, Reps T, et al. A semantics for procedure local heaps and its abstractions. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 2005, 296\u2013309"},{"key":"33_CR8","first-page":"117","volume-title":"Proceedings of the 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering","author":"Y. Chen","year":"2007","unstructured":"Chen Y, Ge L, Hua B, et al. Design of a certifying compiler supporting proof of program safety. In: Proceedings of the 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering. Washington: IEEE Computer Society, 2007, 117\u2013126"},{"issue":"3","key":"33_CR9","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/s11704-007-0029-9","volume":"1","author":"Y. Chen","year":"2007","unstructured":"Chen Y, Ge L, Hua B, et al. A pointer logic and certifying compiler. Frontiers of Computer Science in China. 2007, 1(3):297\u2013312","journal-title":"Frontiers of Computer Science in China"},{"key":"33_CR10","first-page":"230","volume-title":"Proceedings of the ACM SIGPLAN\u201994 Conference on Programing language Design and Implementation","author":"A. Deutsch","year":"1994","unstructured":"Deutsch A. Interprocedural may-alias analysis for pointers: beyond k-limiting. In: Proceedings of the ACM SIGPLAN\u201994 Conference on Programing language Design and Implementation. New York: ACM Press, 1994, 230\u2013241"},{"key":"33_CR11","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Proceedings of the 5th International Conference on Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat R. Proving pointer programs in hoare logic. In: Proceedings of the 5th International Conference on Mathematics of Program Construction. London: Springer, 2000, 102\u2013126"},{"key":"33_CR12","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00289067","volume":"11","author":"R. Topor","year":"1979","unstructured":"Topor R. The correctness of the Schorr-Waite list marking algorithm. Acta Informatica. 1979, 11: 211\u2013221","journal-title":"Acta Informatica"},{"key":"33_CR13","unstructured":"Yang H. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Henglein F, Hughes J, Makholm H, et al. eds. SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. IT University of Copenhagen, 2001, 41\u201368"},{"issue":"1\u20132","key":"33_CR14","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta F, Nipkow T. Proving pointer programs in higherorder logic. Information and Computation. 2005, 199(1\u20132): 200\u2013227","journal-title":"Information and Computation"},{"key":"33_CR15","first-page":"190","volume-title":"Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods","author":"T. Hubert","year":"2005","unstructured":"Hubert T, March\u00e9 C. A case study of C source code verification: the Schorr-Waite algorithm. In: Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods. Washington: IEEE Computer Society, 2005, 190\u2013199"},{"key":"33_CR16","first-page":"259","volume-title":"Computer Science","author":"T. Nipkow","year":"2002","unstructured":"Nipkow T, Paulson L, Wenzel M. Isabelle\/HOL: A proof assistant for higher-order logic. Computer Science. London: Springer, 2002, 259\u2013278"},{"key":"33_CR17","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1093\/comjnl\/42.3.177","volume":"43","author":"R. Bornat","year":"1999","unstructured":"Bornat R, Sufrin B. Animating formal proofs at the surface: the Jape proof calculator. The Computer Journal. 1999, 43: 177\u2013192","journal-title":"The Computer Journal"},{"key":"33_CR18","first-page":"261","volume-title":"Proceedings of the 13th International Static Analysis Symposium","author":"A. Loginov","year":"2006","unstructured":"Loginov A, Reps T, Sagiv M. Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Proceedings of the 13th International Static Analysis Symposium. London: Springer, 2006, 261\u2013279"},{"key":"33_CR19","unstructured":"Cooper D C. Theorem proving in arithmetic without multiplication. In: Meltzer B, Michie D, eds, Machine Intelligence. 1972, 91\u2013100"},{"issue":"10","key":"33_CR20","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM. 1969, 12(10): 576\u2013583","journal-title":"Communications of the ACM"},{"key":"33_CR21","first-page":"1","volume-title":"Proceedings of the 13th European Conference on Object-Oriented Programming","author":"C. A. R. Hoare","year":"1999","unstructured":"Hoare C A R, He J. A trace model for pointers and objects. In: Proceedings of the 13th European Conference on Object-Oriented Programming. London: Springer-Verlag, 1999, 1\u201317"},{"key":"33_CR22","first-page":"115","volume-title":"Proceedings of the 33th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"S. K. Lahiri","year":"2006","unstructured":"Lahiri S K, Qadeer S. Verifying properties of well-founded linked lists. In: Proceedings of the 33th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2006, 115\u2013126"},{"key":"33_CR23","first-page":"19","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee S, Lahiri S K, Qadeer S, et al. A reachability predicate for analyzing low-level software. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. London: Springer, 2007, 19\u201333"},{"key":"33_CR24","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/1328438.1328461","volume-title":"Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"S. K. Lahiri","year":"2008","unstructured":"Lahiri S K, Qadeer S. Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2008, 171\u2013182"},{"key":"33_CR25","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/378795.378851","volume-title":"Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation","author":"A. M\u00f8eller","year":"2001","unstructured":"M\u00f8eller A, Schwartzbach M I. The pointer assertion logic engine. In: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation. New York: ACM Press, 2001, 221\u2013231"},{"issue":"3","key":"33_CR26","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems. 2002, 24(3): 217\u2013298","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"33_CR27","first-page":"177","volume-title":"Selected papers from the 3rd International Workshop on Types in Compilation","author":"D. Walker","year":"2001","unstructured":"Walker D, Morrisett G. Alias types for recursive data structures. In: Selected papers from the 3rd International Workshop on Types in Compilation. London: Springer-Verlag, 2001, 177\u2013206"},{"key":"33_CR28","first-page":"394","volume-title":"the postworkshop proceedings of TYPES 2003","author":"H. Xi","year":"2004","unstructured":"Xi H. Applied type system (extended abstract). In: the postworkshop proceedings of TYPES 2003. Berlin: Springer, 2004, 394\u2013408"},{"key":"33_CR29","first-page":"66","volume-title":"Proceedings of the 10thACM SIGPLAN international conference on Functional programming","author":"C. Chen","year":"2005","unstructured":"Chen C, Xi H. Combining programming with theorem proving. In: Proceedings of the 10thACM SIGPLAN international conference on Functional programming. New York: ACM press, 2005, 66\u201377"},{"key":"33_CR30","first-page":"115","volume-title":"Proceedings of the 4th International Symposium on Formal Methods for Components and Objects","author":"J. Berdine","year":"2005","unstructured":"Berdine J, Calcagno C, O\u2019Hearn P W. Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th International Symposium on Formal Methods for Components and Objects. London: Springer, 2005, 115\u2013137"},{"key":"33_CR31","first-page":"309","volume-title":"Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering","author":"A. Ireland","year":"2006","unstructured":"Ireland A. Towards Automatic Assertion Refinement for Separation Logic. In: Proceedings of the 21st IEEE\/ACM International Conference on Automated Software Engineering. Washington: IEEE Computer Society, 2006, 309\u2013312"},{"key":"33_CR32","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Proceedings of eighth International Conference on Verification, Model Checking and Abstract Interpretation","author":"H. H. Nguyen","year":"2007","unstructured":"Nguyen H H, David C, Qin S, et al. Automated verification of shape and size properties via separation logic. In: Proceedings of eighth International Conference on Verification, Model Checking and Abstract Interpretation. Berlin: Springer, 2007, 251\u2013266"},{"key":"33_CR33","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Proceedings of the 3rd Asian Symposium on Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine J, Calcagno C, O\u2019Hearn P W. Symbolic execution with separation logic. In: Proceedings of the 3rd Asian Symposium on Programming Languages and Systems. London: Springer-Verlag, 2005, 52\u201368"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0033-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-008-0033-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0033-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,19]],"date-time":"2021-09-19T23:16:23Z","timestamp":1632093383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-008-0033-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,5]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["33"],"URL":"https:\/\/doi.org\/10.1007\/s11704-008-0033-8","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"value":"1673-7350","type":"print"},{"value":"1673-7466","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11,5]]}}}