{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T23:40:56Z","timestamp":1684021256204},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sc. China"],"published-print":{"date-parts":[[2007,7]]},"DOI":"10.1007\/s11704-007-0029-9","type":"journal-article","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T15:36:08Z","timestamp":1188401768000},"page":"297-312","source":"Crossref","is-referenced-by-count":8,"title":["A pointer logic and certifying compiler"],"prefix":"10.1007","volume":"1","author":[{"given":"Yiyun","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lin","family":"Ge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baojian","family":"Hua","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhaopeng","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cheng","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhifang","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"G. C. Necula","year":"1997","unstructured":"Necula G C. Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 1997, 106\u2013119"},{"key":"29_CR2","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1145\/268946.268954","volume-title":"Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"J. G. Morrisett","year":"1998","unstructured":"Morrisett J G, Walker D, Crary K, et al. From system F to typed assembly language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 1998, 85\u201397"},{"key":"29_CR3","first-page":"213","volume-title":"Proceedings of the 8th ACM SIGPLAN international conference on Functional programming","author":"Y. Mandelbaum","year":"2003","unstructured":"Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. In: Proceedings of the 8th ACM SIGPLAN international conference on Functional programming. New York: ACM Press, 2003, 213\u2013225"},{"key":"29_CR4","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1109\/LICS.2001.932501","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in computer science","author":"A. W. Appel","year":"2001","unstructured":"Appel A W. Foundational proof-carrying code. In: Proceedings of the 16th Annual IEEE Symposium on Logic in computer science. Washington: IEEE Computer Society, 2001, 247\u2013258"},{"issue":"1\u20133","key":"29_CR5","first-page":"101","volume":"50","author":"D. C. Yu","year":"2004","unstructured":"Yu D C, Hamid N A, Shao Z. Building certified libraries for pcc: dynamic storage allocation. Science of Computer Programming, 2004, 50(1\u20133): 101\u2013127","journal-title":"Science of Computer Programming"},{"key":"29_CR6","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1145\/1133981.1134028","volume-title":"Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation","author":"X. Y. Feng","year":"2006","unstructured":"Feng X Y, Shao Z, Vaynberg A, et al. Modular verification of assembly code with stack-based control abstractions. In: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation. New York: ACM Press, 2006, 401\u2013414"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/978-3-540-24849-1_25","volume-title":"post-workshop Proceedings of TYPES 2003","author":"H. W. Xi","year":"2004","unstructured":"Xi H W. Applied type system (extended abstract). In: post-workshop Proceedings of TYPES 2003. Lecture Notes in Computer Science, Vol 3085. Berlin: Springer-Verlag, 2004, 394\u2013408"},{"key":"29_CR8","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/277650.277752","volume-title":"Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming language design and implementation","author":"G. C. Necula","year":"1998","unstructured":"Necula G C, Lee P. The design and implementation of a certifying compiler. In: Proceedings of the 1998 ACM SIGPLAN Conference on Prgramming language design and implementation. New York: ACM Press, 1998, 333\u2013344"},{"issue":"5","key":"29_CR9","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/358438.349315","volume":"35","author":"C. Colby","year":"2000","unstructured":"Colby C, Lee P, Necula G C, et al. A certifying compiler for Java. ACM SIGPLAN Notices, 2000, 35(5): 95\u2013107","journal-title":"ACM SIGPLAN Notices"},{"key":"29_CR10","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. C. Reynolds","year":"2002","unstructured":"Reynolds J C. 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":"29_CR11","unstructured":"Dijkstra E W. A discipline of programming. Englewood Cliffs, New Jersey: Prentice-Hall, 1976"},{"key":"29_CR12","first-page":"32","volume-title":"Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"B. Steensgaard","year":"1996","unstructured":"Steensgaard B. Points-to analysis in almost linear time. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 1996, 32\u201341"},{"key":"29_CR13","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1145\/781131.781144","volume-title":"Proceedings of the 2003 ACM SIGPLAN Conference on Programming language design and implementation","author":"M. Berndl","year":"2003","unstructured":"Berndl M, Lhot\u00e1k O, Qian F, et al. Points-to analysis using BDDs. In: Proceedings of the 2003 ACM SIGPLAN Conference on Programming language design and implementation. New York: ACM Press, 2003, 103\u2013114"},{"key":"29_CR14","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/379605.379665","volume-title":"Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering","author":"M. Hind","year":"2001","unstructured":"Hind M. Pointer analysis: haven\u2019t we solved this problem yet? In: Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering. New York: ACM Press, 2001, 54\u201361"},{"key":"29_CR15","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-Verlag, 2000, 102\u2013126"},{"key":"29_CR16","first-page":"23","volume-title":"Machine Intelligence","author":"R. M. Burstall","year":"1972","unstructured":"Burstall R M. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, New York: American Elsevier, 1972, 7:23\u201350"},{"issue":"1\u20132","key":"29_CR17","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 higher-order logic. Information and Computation, 2005, 199(1\u20132): 200\u2013227","journal-title":"Information and Computation"},{"key":"29_CR18","first-page":"15","volume-title":"Proceedings of the 6th International conference on formal engineering methods","author":"J. C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre J C, March\u00e9 C. Multi-Prover Verification of C Programs. In: Proceedings of the 6th International conference on formal engineering methods. Seattle: Springer-Verlag, 2004, 15\u201329"},{"key":"29_CR19","volume-title":"Piton: a mechanically verified assembly-language","author":"J. S. Moore","year":"1996","unstructured":"Moore J S. Piton: a mechanically verified assembly-language. Norwell: Kluwer Academic Publishers, 1996"},{"key":"29_CR20","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"X. Leroy","year":"2006","unstructured":"Leroy X. Formal certification of a compiler back-end or programming a compiler with a proof assistant. In: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 2006, 42\u201354"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-007-0029-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-007-0029-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-007-0029-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T23:21:28Z","timestamp":1684020088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-007-0029-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["29"],"URL":"https:\/\/doi.org\/10.1007\/s11704-007-0029-9","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"value":"1673-7350","type":"print"},{"value":"1673-7466","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7]]}}}