{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T10:40:20Z","timestamp":1741257620824,"version":"3.38.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"10","license":[{"start":{"date-parts":[[2011,6,17]],"date-time":"2011-06-17T00:00:00Z","timestamp":1308268800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2011,10]]},"DOI":"10.1007\/s11432-011-4300-1","type":"journal-article","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T08:21:36Z","timestamp":1308385296000},"page":"2013-2027","source":"Crossref","is-referenced-by-count":1,"title":["A verifiable low-level concurrent programming model based on colored Petri nets"],"prefix":"10.1007","volume":"54","author":[{"given":"ShengYuan","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,6,17]]},"reference":[{"key":"4300_CR1","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1002\/spe.438","volume":"32","author":"Leroy. Xavier","year":"2002","unstructured":"Xavier Leroy. Bytecode verification for Java smart card. Software Practice Experience, 2002, 32: 319\u2013340","journal-title":"Software Practice Experience"},{"key":"4300_CR2","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/277650.277752","volume-title":"PLDI\u2019 98 Proceedings of the ACM SIGPLAN 1998 Conference on Programming 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: PLDI\u2019 98 Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, New York: ACM, 1998. 333\u2013344"},{"key":"4300_CR3","first-page":"28","volume":"1473","author":"G. Morrisett","year":"1998","unstructured":"Morrisett G, Crary K, Glew N, et al. Stack-based typed assembly language. Comput Sci, 1998, 1473: 28\u201352","journal-title":"Comput Sci"},{"key":"4300_CR4","unstructured":"Morrisett G, Crary K, Glew N, et al. TALx86: A realistic typed assembly language. In: Proceedings of Workshop on Compiler Support for System Software, ACM SIGPLAN, 1999. 25\u201335"},{"key":"4300_CR5","volume-title":"POPL\u2019 99 Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A.C. Myers","year":"1999","unstructured":"Myers AC. Jflow: Practical mostly-static information flow control. In: POPL\u2019 99 Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York: ACM, 1999"},{"key":"4300_CR6","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.scico.2004.01.003","volume":"50","author":"D. C. Yu","year":"2004","unstructured":"Yu D C, Hamid N A, Shao Z. Building certified lbraries for PCC: Dynamic storage allocation. Sci Comput Programming, 2004, 50: 101\u2013127","journal-title":"Sci Comput Programming"},{"key":"4300_CR7","first-page":"215","volume-title":"Proceedings of 10th International Conference","author":"L. Burdy","year":"2007","unstructured":"Burdy L, Huisman M, Pavlova M. Preliminary design of BML: A behavioral interface specification language for java bytecode. In: Proceedings of 10th International Conference, FASE Heidelberg: Springer-Verlag Berlin, 2007. 215\u2013229"},{"key":"4300_CR8","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1165389.945448","volume":"37","author":"R. Sekar","year":"2003","unstructured":"Sekar R, Venkatakrishnan V N, Basu S, et al. Model-carrying code: A practical approach for safe execution of untrusted applications. ACM SIGOPS Operating Syst Rev, 2003, 37: 15\u201328","journal-title":"ACM SIGOPS Operating Syst Rev"},{"key":"4300_CR9","volume-title":"ICFP\u2019 04 Proceedings of the ninth ACM SIGPLAN International Conference on Functional Programming","author":"D.C. Yu","year":"2004","unstructured":"Yu DC, Shao Z. Verification of safety properties for concurrent assembly code. In: ICFP\u2019 04 Proceedings of the ninth ACM SIGPLAN International Conference on Functional Programming, Snowbird: ACM, 2004"},{"key":"4300_CR10","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C. A. R. Hoare","year":"1978","unstructured":"Hoare C A R. Communicating sequential processes. Commun ACM, 1978, 21: 666\u2013677","journal-title":"Commun ACM"},{"key":"4300_CR11","volume-title":"Communicating and Mobile Systems: The \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner R. Communicating and Mobile Systems: The \u03c0-Calculus. Cambridge: Cambridge University Press, 1999"},{"key":"4300_CR12","series-title":"EATCS monographs on Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri Nets: An Introduction","author":"W. Resig","year":"1985","unstructured":"Resig W. Petri Nets: An Introduction, vol.4 of EATCS monographs on Theoretical Computer Science. Berlin: Springer, 1985"},{"key":"4300_CR13","volume-title":"Parallel Program Design A Foundation","author":"K. M. Chandy","year":"1988","unstructured":"Chandy K M, Misra J. Parallel Program Design A Foundation. MA: Addison-Wesley Publishing Company, Inc., 1988"},{"key":"4300_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-06289-0","volume-title":"Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 1, EATCS Monographs in Computer Science","author":"K. Jensen","year":"1992","unstructured":"Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Volume 1, EATCS Monographs in Computer Science. Heidelberg: Springer, 1992"},{"key":"4300_CR15","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. Commun ACM, 1969, 12: 576\u2013580","journal-title":"Commun ACM"},{"key":"4300_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume":"2142","author":"P. W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn P W, Reynolds J C, Yang H. Local reasoning about programs that alter data structures. Comput Sci Logic, 2001, 2142: 1\u201319","journal-title":"Comput Sci Logic"},{"key":"4300_CR17","unstructured":"Reynolds J C. Separation logic: a logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, 2002. 55\u201374"},{"key":"4300_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-05324-9","volume-title":"Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications","author":"C. Girault","year":"2003","unstructured":"Girault C, Valk R. Petri Nets for System Engineering: A Guide to Modeling, Verification, and Applications. Berlin: Springer, 2003"},{"key":"4300_CR19","unstructured":"Liang Y Y. Study on verification of concurrent low-level programs based on certifying compilers. Dissertation ofMaster\u2019s Degree, Tsinghua University, 2007"},{"key":"4300_CR20","first-page":"259","volume-title":"POPL\u201905 Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages","author":"R. Bornat","year":"2005","unstructured":"Bornat R, Calcagno C, Peter O\u2019Hearn, et al. Permission accounting in separation logic. In POPL\u201905 Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages. New York: ACM Press, 2005. 259\u2013270"},{"key":"4300_CR21","doi-asserted-by":"crossref","unstructured":"Hayman J, Winskel G. Independence and concurrent separation logic. In: 21st Annual IEEE Symposium on Logic in Computer Science, Seattle, 2006. 147\u2013156","DOI":"10.1109\/LICS.2006.30"},{"key":"4300_CR22","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P. W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn P W. Resources, concurrency and local reasoning. Theor Comput Sci, 2007, 375: 271\u2013307","journal-title":"Theor Comput Sci"},{"key":"4300_CR23","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/MM.2007.63","volume":"3","author":"T. Harris","year":"2007","unstructured":"Harris T, Cristal A, Unsal O S, et al. Transactional memory: An overview. IEEE Micro, 2007, 3: 8\u201329","journal-title":"IEEE Micro"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-011-4300-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-011-4300-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-011-4300-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T09:47:20Z","timestamp":1741254440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-011-4300-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,17]]},"references-count":23,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["4300"],"URL":"https:\/\/doi.org\/10.1007\/s11432-011-4300-1","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"type":"print","value":"1674-733X"},{"type":"electronic","value":"1869-1919"}],"subject":[],"published":{"date-parts":[[2011,6,17]]}}}