{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:51:45Z","timestamp":1770281505860,"version":"3.49.0"},"reference-count":13,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,7,31]],"date-time":"2012-07-31T00:00:00Z","timestamp":1343692800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Separation logic is a concise method for specifying programs that manipulate\ndynamically allocated storage. Partially inspired by separation logic, Implicit\nDynamic Frames has recently been proposed, aiming at first-order tool support.\nIn this paper, we precisely connect the semantics of these two logics. We\ndefine a logic whose syntax subsumes both that of a standard separation logic,\nand that of implicit dynamic frames as sub-syntaxes. We define a total heap\nsemantics for our logic, and, for the separation logic subsyntax, prove it\nequivalent the standard partial heaps model. In order to define a semantics\nwhich works uniformly for both subsyntaxes, we define the novel concept of a\nminimal state extension, which provides a different (but equivalent) definition\nof the semantics of separation logic implication and magic wand connectives,\nwhile also giving a suitable semantics for these connectives in implicit\ndynamic frames. We show that our resulting semantics agrees with the existing\ndefinition of weakest pre-condition semantics for the implicit dynamic frames\nfragment. Finally, we show that we can encode the separation logic fragment of\nour logic into the implicit dynamic frames fragment, preserving semantics. For\nthe connectives typically supported by tools, this shows that separation logic\ncan be faithfully encoded in a first-order automatic verification tool\n(Chalice).<\/jats:p>","DOI":"10.2168\/lmcs-8(3:1)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":19,"title":["The Relationship Between Separation Logic and Implicit Dynamic Frames"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Matthew J.","family":"Parkinson","sequence":"first","affiliation":[]},{"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,7,31]]},"reference":[{"key":"10.2168\/LMCS-8(3:1)2012_cminor","doi-asserted-by":"crossref","unstructured":"A. W. Appel and S. Blazy. Separation logic for small-step Cminor. InTPHOLs, pages 5-21, 2007.","DOI":"10.1007\/978-3-540-74591-4_3"},{"key":"10.2168\/LMCS-8(3:1)2012_benton-leperchey","doi-asserted-by":"crossref","unstructured":"N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. InTLCA, 2005.","DOI":"10.1007\/11417170_8"},{"key":"10.2168\/LMCS-8(3:1)2012_bornat05","doi-asserted-by":"crossref","unstructured":"R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. InPOPL, pages 259-270, 2005.","DOI":"10.1145\/1047659.1040327"},{"key":"10.2168\/LMCS-8(3:1)2012_boyland03","doi-asserted-by":"crossref","unstructured":"J. Boyland. Checking interference with fractional permissions. InSAS, 2003.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"10.2168\/LMCS-8(3:1)2012_Kassios_thesis","unstructured":"I. T. Kassios.A Theory of Object Oriented Refinement. PhD thesis, 2006."},{"key":"10.2168\/LMCS-8(3:1)2012_LeinoBoogie2","unstructured":"K. R. M. Leino. This is Boogie 2. Available from http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers.html."},{"key":"10.2168\/LMCS-8(3:1)2012_LeinoM09","doi-asserted-by":"crossref","unstructured":"K. R. M. Leino and P. M\u00fcller. A basis for verifying multi-threaded programs. InESOP, pages 378-393, 2009.","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"10.2168\/LMCS-8(3:1)2012_ohearn:csljournal","unstructured":"P. W. O'Hearn. Resources, concurrency and local reasoning.TCS, 2007."},{"key":"10.2168\/LMCS-8(3:1)2012_ohearn04","doi-asserted-by":"crossref","unstructured":"P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. InPOPL, pages 268-280, 2004.","DOI":"10.1145\/982962.964024"},{"key":"10.2168\/LMCS-8(3:1)2012_parkinson_thesis","unstructured":"M. Parkinson.Local Reasoning for Java. PhD thesis, University of Cambridge, November 2005."},{"key":"10.2168\/LMCS-8(3:1)2012_Rustan10dafny:an","unstructured":"K. Rustan and M. Leino. Dafny: An automatic program verifier for functional correctness. InLPAR, 2010."},{"key":"10.2168\/LMCS-8(3:1)2012_Smans_thesis","unstructured":"J. Smans.Specification and Automatic Verification of Frame Properties for Java-like Programs (Specificatie en automatische verificatie van frame eigenschappen voor Java-achtige programma singles). PhD thesis, FWO-Vlaanderen, May 2009."},{"key":"10.2168\/LMCS-8(3:1)2012_SmansJP10","doi-asserted-by":"crossref","unstructured":"J. Smans, B. Jacobs, and F. Piessens. Heap-dependent expressions in separation logic. InFMOODS\/FORTE, pages 170-185, 2010.","DOI":"10.1007\/978-3-642-13464-7_14"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/802\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/802\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:29Z","timestamp":1681242989000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,31]]},"references-count":13,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:1)2012","relation":{"references":[{"id-type":"doi","id":"10.1145\/1040305.1040327","asserted-by":"subject"},{"id-type":"doi","id":"10.1145\/1047659.1040327","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1203.6859","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.6859","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,31]]},"article-number":"802"}}