{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T11:10:11Z","timestamp":1745406611344,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642351815"},{"type":"electronic","value":"9783642351822"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35182-2_24","type":"book-chapter","created":{"date-parts":[[2012,12,6]],"date-time":"2012-12-06T01:19:15Z","timestamp":1354756755000},"page":"332-349","source":"Crossref","is-referenced-by-count":5,"title":["A Case for Behavior-Preserving Actions in Separation Logic"],"prefix":"10.1007","author":[{"given":"David","family":"Costanzo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"A.W. Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation Logic for Small-Step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 5\u201321. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proc. 20th IEEE Symp. on Logic in Computer Science, pp. 260\u2013269 (2005)","key":"24_CR2","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"24_CR3","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. 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)"},{"doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 366\u2013378 (July 2007)","key":"24_CR4","DOI":"10.1109\/LICS.2007.30"},{"doi-asserted-by":"crossref","unstructured":"Costanzo, D., Shao, Z.: A case for behavior-preserving actions in separation logic. Technical report, Dept. of Computer Science, Yale University, New Haven, CT (June 2012), http:\/\/flint.cs.yale.edu\/publications\/bpsl.html","key":"24_CR5","DOI":"10.1007\/978-3-642-35182-2_24"},{"issue":"5","key":"24_CR6","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/s00165-009-0125-8","volume":"22","author":"I. Filipovic","year":"2010","unstructured":"Filipovic, I., O\u2019Hearn, P.W., Torp-Smith, N., Yang, H.: Blaming the client: on data refinement in the presence of pointers. Formal Asp. Comput.\u00a022(5), 547\u2013583 (2010)","journal-title":"Formal Asp. Comput."},{"unstructured":"Huet, G., Paulin-Mohring, C., et al.: The Coq proof assistant reference manual. The Coq release v6.3.1 (May 2000)","key":"24_CR7"},{"doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM Symposium on Principles of Programming Languages, pp. 14\u201326 (January 2001)","key":"24_CR8","DOI":"10.1145\/373243.375719"},{"unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice Hall (1988)","key":"24_CR9"},{"key":"24_CR10","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)"},{"issue":"3","key":"24_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1498926.1498929","volume":"31","author":"P.W. O\u2019Hearn","year":"2009","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM Trans. Program. Lang. Syst.\u00a031(3), 1\u201350 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Raza, M., Gardner, P.: Footprints in local reasoning. Journal of Logical Methods in Computer Science 5(2) (2009)","key":"24_CR12","DOI":"10.2168\/LMCS-5(2:4)2009"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symp. on Logic in Computer Science, pp. 55\u201374 (July 2002)","key":"24_CR13","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1-3","key":"24_CR14","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. Theor. Comput. Sci.\u00a0375(1-3), 308\u2013334 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR15","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.W.: 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-35182-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T10:34:51Z","timestamp":1745404491000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35182-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351815","9783642351822"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35182-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}