{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:44Z","timestamp":1725559244736},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_34","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"485-489","source":"Crossref","is-referenced-by-count":6,"title":["Separation Logic Adapted for Proofs by Rewriting"],"prefix":"10.1007","author":[{"given":"Magnus O.","family":"Myreen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"34_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 (TPHOLs)","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)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-71067-7_18","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Gast","year":"2008","unstructured":"Gast, H.: Lightweight separation. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 199\u2013214. Springer, Heidelberg (2008)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-71067-7_4","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Kaufmann","year":"2008","unstructured":"Kaufmann, M., Moore, J.S.: An ACL2 tutorial. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 17\u201321. Springer, Heidelberg (2008)"},{"key":"34_CR4","volume-title":"Workshop of the Japan Society for Software Science and Technology","author":"N. Marti","year":"2005","unstructured":"Marti, N., Aeldt, R., Yonezawa, A.: Towards formal verification of memory properties using separation logic. In: Workshop of the Japan Society for Software Science and Technology, Japan Society for Software Science and Technology, Japan (2005)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"TPHOLs","author":"A. McCreight","year":"2009","unstructured":"McCreight, A.: Practical tactics for separation logic. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 343\u2013358. Springer, Heidelberg (2009)"},{"unstructured":"Myreen, M.O., Kaufmann, M.: HOL4 and ACL2 implementations, HOL4 (Myreen): ACL2 (Kaufmann), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~mom22\/sep-rewrite\/","key":"34_CR6"},{"key":"34_CR7","volume-title":"Proceedings of Logic in Computer Science (LICS)","author":"J. Reynolds","year":"2002","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Proceedings of Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos (2002)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"34_CR9","first-page":"97","volume-title":"Principles of Programming Languages (POPL)","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Principles of Programming Languages (POPL), pp. 97\u2013108. ACM, New York (2007)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"TPHOLs","author":"T. Tuerk","year":"2009","unstructured":"Tuerk, T.: A formalisation of smallfoot in HOL. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 469\u2013484. Springer, Heidelberg (2009)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-30124-0_21","volume-title":"Computer Science Logic","author":"T. Weber","year":"2004","unstructured":"Weber, T.: Towards mechanized program verification with separation logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 250\u2013264. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:25Z","timestamp":1619785045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}