{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:40Z","timestamp":1779087580860,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540713142","type":"print"},{"value":"9783540713166","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_13","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:58:28Z","timestamp":1184605108000},"page":"173-188","source":"Crossref","is-referenced-by-count":53,"title":["On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning"],"prefix":"10.1007","author":[{"given":"Xinyu","family":"Feng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rodrigo","family":"Ferreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Bornat, R., et al.: Permission accounting in separation logic. In: Proc. 32nd ACM Symp. on Principles of Prog. Lang, pp. 259\u2013270 (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S. Brookes","year":"2004","unstructured":"Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Brookes, S.: A grainless semantics for parallel programs with shared mutable data. In: Proc. MFPS XXI. Electr. Notes Theor. Comput. Sci., vol.\u00a0155, pp. 277\u2013307 (2006)","DOI":"10.1016\/j.entcs.2005.11.060"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. Technical Report YALEU\/DCS\/TR-1374 and Formulation in Coq, Dept. of Computer Science, Yale University, New Haven, CT (January 2007)","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z.: Modular verification of concurrent assembly code with dynamic thread creation and termination. In: Proc. ICFP\u201905, Tallinn, Estonia, pp. 254\u2013267 (2005)","DOI":"10.1145\/1086365.1086399"},{"key":"13_CR6","first-page":"61","volume-title":"Operating Systems Techniques","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: Hoare, C.A.R., Perrott, R.H. (eds.) Operating Systems Techniques, pp. 61\u201371. Academic Press, London (1972)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM Symp. on Principles of Prog. Lang, pp. 14\u201326 (2001)","DOI":"10.1145\/360204.375719"},{"issue":"4","key":"13_CR8","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"13_CR9","first-page":"106","volume-title":"Proc. 24th ACM Symp. on Principles of Prog. Lang.","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: Proc. 24th ACM Symp. on Principles of Prog. Lang., Jan. 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"13_CR10","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science (to appear)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 49\u201367. Springer, Heidelberg (2004)"},{"issue":"5","key":"13_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. In: Proc. 34th ACM Symp. on Principles of Prog. Lang., to appear. ACM Press (Jan. 2007)","DOI":"10.1145\/1190216.1190261"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS\u201902, July 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-3-540-30538-5_4","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J.C. Reynolds","year":"2004","unstructured":"Reynolds, J.C.: Toward a grainless semantics for shared-variable concurrency. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 35\u201348. Springer, Heidelberg (2004)"},{"key":"13_CR16","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. The Coq release v8.0 (Oct. 2004)"},{"key":"13_CR17","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic (2007), Available at http:\/\/www.cl.cam.ac.uk\/~mjp41\/RGSep.pdf"},{"issue":"1","key":"13_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: Proc. 2004 ACM SIGPLAN Int\u2019l Conf. on Functional Prog., September 2004, pp. 175\u2013188 (2004)","DOI":"10.21236\/ADA436482"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71316-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T03:49:48Z","timestamp":1556682588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}