{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:26Z","timestamp":1774837826694,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_24","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"343-358","source":"Crossref","is-referenced-by-count":33,"title":["Practical Tactics for Separation Logic"],"prefix":"10.1007","author":[{"given":"Andrew","family":"McCreight","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, Washington, DC, USA, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"24_CR3","first-page":"220","volume-title":"POPL 2005","author":"L. Birkedal","year":"2004","unstructured":"Birkedal, L., Torp-Smith, N., Reynolds, J.C.: Local reasoning about a copying garbage collector. In: POPL 2005, pp. 220\u2013231. ACM Press, New York (2004)"},{"key":"24_CR4","first-page":"468","volume-title":"PLDI 2007","author":"A. McCreight","year":"2007","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying gcs and their mutators. In: PLDI 2007, pp. 468\u2013479. ACM, New York (2007)"},{"key":"24_CR5","unstructured":"The Coq Development Team: The Coq proof assistant, \n                    \n                      http:\/\/coq.inria.fr"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"24_CR7","first-page":"42","volume-title":"POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"issue":"11","key":"24_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1145\/362790.362798","volume":"13","author":"C.J. Cheney","year":"1970","unstructured":"Cheney, C.J.: A nonrecursive list compacting algorithm. Communications of the ACM\u00a013(11), 677\u2013678 (1970)","journal-title":"Communications of the ACM"},{"key":"24_CR9","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)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq\u2014rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"},{"key":"24_CR12","unstructured":"Appel, A.W.: Tactics for separation logic (January 2006), \n                    \n                      http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N. Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an os using separation logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 400\u2013419. Springer, Heidelberg (2006)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD) (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"24_CR16","first-page":"441","volume-title":"POPL 2009","author":"C. Hawblitzel","year":"2009","unstructured":"Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: POPL 2009, pp. 441\u2013453. ACM, New York (2009)"},{"key":"24_CR17","first-page":"97","volume-title":"POPL 2007","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL 2007, pp. 97\u2013108. ACM, New York (2007)"},{"key":"24_CR18","unstructured":"Marti, N., Affeldt, R.: A certified verifier for a fragment of separation logic. In: 9th JSSST Workshop on Programming and Prog. Langs, PPL 2007 (2007)"},{"key":"24_CR19","unstructured":"Tuerk, T.: A separation logic framework in HOL. In: Otmane Ait Mohamed, C.M., Tahar, S. (eds.) TPHOLs 2008: Emerging Trends Proceedings, August 2008, pp. 116\u2013122 (2008)"},{"key":"24_CR20","first-page":"289","volume-title":"POPL 2009","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009, pp. 289\u2013300. ACM, New York (2009)"},{"issue":"1-2","key":"24_CR21","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.ic.2004.10.007","volume":"199","author":"F. Mehta","year":"2005","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput.\u00a0199(1-2), 200\u2013227 (2005)","journal-title":"Inf. Comput."},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:41:34Z","timestamp":1552120894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}