{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:43Z","timestamp":1775790703732,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540744061","type":"print"},{"value":"9783540744078","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74407-8_18","type":"book-chapter","created":{"date-parts":[[2007,8,18]],"date-time":"2007-08-18T14:30:48Z","timestamp":1187447448000},"page":"256-271","source":"Crossref","is-referenced-by-count":127,"title":["A Marriage of Rely\/Guarantee and Separation Logic"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Vafeiadis","sequence":"first","affiliation":[]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Prog. Lang. Syst.\u00a017(3), 507\u2013534 (1995)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"18_CR2","first-page":"247","volume":"155","author":"R. Bornat","year":"2006","unstructured":"Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. ENTCS\u00a0155, 247\u2013276 (2006)","journal-title":"ENTCS"},{"key":"18_CR3","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.D. Brookes","year":"2004","unstructured":"Brookes, S.D.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/1190216.1190236","volume-title":"POPL","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: POPL, pp. 123\u2013134. ACM Press, New York (2007)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. LICS (to appear, 2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"SAS","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: SAS. LNCS, Springer, Heidelberg (2007)"},{"key":"18_CR7","unstructured":"Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely\/guarantee rules. Technical Report CS-TR-987, Newcastle University (October 2006)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: Proceedings of ESOP (2007)","DOI":"10.1007\/978-3-540-71316-6_13"},{"issue":"10","key":"18_CR9","doi-asserted-by":"publisher","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\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. Operating Systems Techniques (1971)","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"18_CR11","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"18_CR12","first-page":"5","volume-title":"Wanted: a compositional approach to concurrency","author":"C.B. Jones","year":"2003","unstructured":"Jones, C.B.: Wanted: a compositional approach to concurrency, pp. 5\u201315. Springer, New York (2003)"},{"issue":"3","key":"18_CR13","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C. Morgan","year":"1988","unstructured":"Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst.\u00a010(3), 403\u2013419 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL, pp. 1\u201319 (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"18_CR15","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)"},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica\u00a06, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., O\u2019Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL (2007)","DOI":"10.1145\/1190216.1190261"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"L. Prensa Nieto","year":"2003","unstructured":"Prensa Nieto, L.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 348\u2013362. Springer, Heidelberg (2003)"},{"key":"18_CR19","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, Washington, DC, USA, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"18_CR20","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":"18_CR21","volume-title":"PPoPP","author":"V. Vafeiadis","year":"2006","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP, ACM Press, New York (2006)"},{"key":"18_CR22","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. Technical Report UCAM-CL-TR-687, University of Cambridge (June 2007), http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-687.html"},{"issue":"2","key":"18_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing\u00a09(2), 149\u2013174 (1997)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2007 \u2013 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74407-8_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T20:57:45Z","timestamp":1684011465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74407-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744061","9783540744078"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}