{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:05:36Z","timestamp":1770271536498,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540766360","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-76637-7_3","type":"book-chapter","created":{"date-parts":[[2007,11,20]],"date-time":"2007-11-20T07:47:52Z","timestamp":1195544872000},"page":"19-37","source":"Crossref","is-referenced-by-count":47,"title":["Local Reasoning for Storable Locks and Threads"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Gotsman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josh","family":"Berdine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.: Permission accounting in separation logic. In: POPL (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","first-page":"227","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S.D. Brookes","year":"2004","unstructured":"Brookes, S.D.: A semantics of concurrent separation logic. Theoretical Computer Science\u00a0375(1-3), 227\u2013270 In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 227\u2013270. Springer, Heidelberg (2004)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: LICS (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: ESOP (2007)","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z.: Modular verification of concurrent assembly code with dynamic thread creation and termination. In: ICFP (2005)","DOI":"10.1145\/1086365.1086399"},{"key":"3_CR6","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. Technical Report MSR-TR-2007-39, Microsoft Research (April 2007)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: CSL (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"issue":"1-3","key":"3_CR10","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007) Preliminary version appeared in CONCUR 2004","journal-title":"Theoretical Computer Science"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., Calcagno, C.: Variables as resource in Hoare logics. In: LICS (2006)","DOI":"10.1109\/LICS.2006.52"},{"key":"3_CR13","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: CONCUR 2007. LNCS, vol.\u00a04703, Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-76637-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:56:26Z","timestamp":1619520986000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-76637-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540766360"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-76637-7_3","relation":{},"subject":[]}}