{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T07:25:35Z","timestamp":1769066735594,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119569","type":"print"},{"value":"9783642119576","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_15","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"267-286","source":"Crossref","is-referenced-by-count":23,"title":["Parameterized Memory Models and Concurrent Separation Logic"],"prefix":"10.1007","author":[{"given":"Rodrigo","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"12","key":"15_CR1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. Adve","year":"1996","unstructured":"Adve, S., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029(12), 66\u201376 (1996)","journal-title":"IEEE Computer"},{"issue":"6","key":"15_CR2","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"S. Adve","year":"1993","unstructured":"Adve, S., Hill, M.: A unified formalization of four shared-memory models. IEEE Transactions on Parallel and Distributed Systems\u00a04(6), 613\u2013624 (1993)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: 31st POPL, January 2004, pp. 14\u201325 (2004)","DOI":"10.1145\/964001.964003"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Boehm, H., Adve, S.: The foundations of the C++ concurrency memory model. In: PLDI, Tucson, Arizona, June 2008, pp. 68\u201378 (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J.: Threads cannot be implemented as a library. In: PLDI, Chicago, June 2005, pp. 261\u2013268 (2005)","DOI":"10.1145\/1065010.1065042"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: 32nd POPL, January 2005, pp. 259\u2013270 (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: 36th POPL, Savannah, Georgia, USA, January 2009, pp. 392\u2013403 (2009)","DOI":"10.1145\/1594834.1480930"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/j.entcs.2005.11.060","volume":"155","author":"S. Brookes","year":"2006","unstructured":"Brookes, S.: A grainless semantics for parallel programs with shared mutable data. Electronic Notes in Theoretical Computer Science\u00a0155, 277\u2013307 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1-3","key":"15_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theoretical Comp. Sci.\u00a0375(1-3), 227\u2013270 (2007)","journal-title":"Theoretical Comp. Sci."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: 22nd LICS, July 2007, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-71316-6_23","volume-title":"Programming Languages and Systems","author":"P. Cenciarelli","year":"2007","unstructured":"Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 331\u2013346. Springer, Heidelberg (2007)"},{"key":"15_CR12","first-page":"43","volume-title":"Programming Languages","author":"E. Dijkstra","year":"1968","unstructured":"Dijkstra, E.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43\u2013112. Academic Press, London (1968)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: 36th POPL, January 2009, pp. 315\u2013327 (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X. Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic (extended version). Technical Report YALEU\/DCS\/TR-1422, Department of Computer Science, Yale University (2009), http:\/\/flint.cs.yale.edu\/publications\/rmm.html","DOI":"10.1007\/978-3-642-11957-6_15"},{"issue":"8","key":"15_CR16","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1109\/12.868026","volume":"49","author":"G. Gao","year":"2000","unstructured":"Gao, G., Sarkar, V.: Location consistency \u2013 a new memory model and cache consistency protocol. IEEE Transactions on Computers\u00a049(8), 798\u2013813 (2000)","journal-title":"IEEE Transactions on Computers"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A., Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers\u00a028(9) (September 1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: 33rd POPL, January 2006, pp. 42\u201354 (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: 32nd POPL, Long Beach, California, January 2005, pp. 378\u2013391 (2005)","DOI":"10.1145\/1040305.1040336"},{"issue":"1","key":"15_CR22","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/160551.160553","volume":"27","author":"D. Mosberger","year":"1993","unstructured":"Mosberger, D.: Memory consistency models. Operating Systems Review\u00a027(1), 18\u201326 (1993)","journal-title":"Operating Systems Review"},{"issue":"1-3","key":"15_CR23","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.: Resources, concurrency, and local reasoning. Theoretical Comp. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Comp. Sci."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: 22nd TPHOLS, Munich, Germany, August 2009, pp. 391\u2013407 (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"15_CR25","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. Reynolds","year":"2004","unstructured":"Reynolds, J.: 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":"15_CR26","doi-asserted-by":"crossref","unstructured":"Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: 12th PPoPP, San Jose (March 2007)","DOI":"10.1145\/1229428.1229469"},{"key":"15_CR27","unstructured":"Sevcik, J.: Program Transformations in Weak Memory Models. PhD thesis, School of Informatics, University of Edinburgh (2008)"},{"key":"15_CR28","unstructured":"SPARC International Inc. The SPARC Architecture Manual, Version 8. Revision SAV080SI9308 (1992)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"issue":"1-3","key":"15_CR30","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H. Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. Theoretical Computer Science\u00a0375(1-3), 308\u2013334 (2007)","journal-title":"Theoretical Computer Science"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-45931-6_28","volume-title":"Foundations of Software Science and Computation Structures","author":"H. Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 402\u2013416. Springer, Heidelberg (2002)"}],"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-642-11957-6_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T19:56:27Z","timestamp":1685476587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}