{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:19:15Z","timestamp":1766135955096},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_49","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"460-469","source":"Crossref","is-referenced-by-count":11,"title":["An Overview of Separation Logic"],"prefix":"10.1007","author":[{"given":"John C.","family":"Reynolds","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"49_CR1","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Houndsmill, Hampshire, Palgrave, pp. 303\u2013321 (2000)"},{"key":"49_CR2","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14\u201326. ACM, New York (2001)"},{"key":"49_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","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. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, Springer, Heidelberg (2001)"},{"key":"49_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, California","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, California, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"49_CR5","unstructured":"Yang, H.: An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm. In: Henglein, F., Hughes, J., Makholm, H., Niss, H. (eds.) SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, IT University of Copenhagen, pp. 41\u201368 (2001)"},{"key":"49_CR6","unstructured":"Yang, H.: Local Reasoning for Stateful Programs. Ph.\u00a0D. dissertation, University of Illinois, Urbana-Champaign, Illinois (2001)"},{"key":"49_CR7","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1145\/964001.964020","volume-title":"Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"L. Birkedal","year":"2004","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 220\u2013231. ACM Press, New York (2004)"},{"key":"49_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C. Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"49_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"49_CR10","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/964001.964024","volume-title":"Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Conference Record of POPL 2004: The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 268\u2013280. ACM Press, New York (2004)"},{"key":"49_CR11","volume-title":"Proceedings Twentieth Annual IEEE Symposium on Logic in Computer Science","author":"L. Birkedal","year":"2005","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proceedings Twentieth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, California, IEEE Computer Society, Los Alamitos (2005)"},{"key":"49_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: Bi-hyperdoctrines and higher order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"49_CR13","doi-asserted-by":"crossref","unstructured":"Mijajlovi\u0107, I., Torp-Smith, N.: Refinement in a separation context. In: SPACE 2004: Informal Proceedings of Second Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (2004)","DOI":"10.1007\/978-3-540-30538-5_35"},{"key":"49_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-540-30538-5_35","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"I. Mijajlovi\u0107","year":"2004","unstructured":"Mijajlovi\u0107, I., Torp-Smith, N., O\u2019Hearn, P.W.: Refinement and separation contexts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 421\u2013433. Springer, Heidelberg (2004)"},{"key":"49_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"49_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"49_CR17","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/1040305.1040327","volume-title":"Conference Record of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.: Permission accounting in separation logic. In: Conference Record of POPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259\u2013270. ACM Press, New York (2005)"},{"key":"49_CR18","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.scico.2004.01.003","volume":"50","author":"D. Yu","year":"2004","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming\u00a050, 101\u2013127 (2004)","journal-title":"Science of Computer Programming"},{"key":"49_CR19","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/S0304-3975(02)00868-X","volume":"298","author":"C. Calcagno","year":"2003","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Computer Science\u00a0298, 557\u2013581 (2003)","journal-title":"Theoretical Computer Science"},{"key":"49_CR20","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Research Report YALEU\/CS\/TR-1294, Yale University, New Haven, Connecticut (2005), http:\/\/flint.cs.yale.edu\/flint\/publications\/xcap.html","DOI":"10.1145\/1111037.1111066"},{"key":"49_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-45332-6_7","volume-title":"Types in Compilation","author":"D. Walker","year":"2001","unstructured":"Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol.\u00a02071, pp. 177\u2013206. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_49","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T10:44:17Z","timestamp":1684493057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}