{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:42Z","timestamp":1779074682904,"version":"3.51.4"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"3-4","license":[{"start":{"date-parts":[[2019,8,1]],"date-time":"2019-08-01T00:00:00Z","timestamp":1564617600000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"},{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"crossref","award":["1228695"],"award-info":[{"award-number":["1228695"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"crossref","award":["1518789"],"award-info":[{"award-number":["1518789"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Framing is important for specification and verification, especially in programs that mutate data structures with shared data, such as DAGs. Both separation logic and region logic are successful approaches to framing, with separation logic providing a concise way to reason about data structures that are disjoint, and region logic providing the ability to reason about framing for shared mutable data. In order to obtain the benefits of both logics for programs with shared mutable data, this paper unifies them into a single logic, which can encode both of them and allows them to interoperate. The new logic thus provides a way to reason about program modules specified in a mix of styles.<\/jats:p>","DOI":"10.1007\/s00165-018-0455-5","type":"journal-article","created":{"date-parts":[[2018,5,25]],"date-time":"2018-05-25T09:04:29Z","timestamp":1527239069000},"page":"381-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Unifying separation logic and region logic to allow interoperability"],"prefix":"10.1145","volume":"30","author":[{"given":"Yuyan","family":"Bao","sequence":"first","affiliation":[{"name":"University of Central Florida, 32816, Orlando, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"University of Central Florida, 32816, Orlando, FL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Augsburg, 86135, Augsburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","first-page":"364","volume-title":"Formal methods for components and objects (FMCO) 2005, revised lectures (Lecture notes in computer science)","author":"Barnett M","year":"2006"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barrett C Conway CL Deters M Hadarean L Jovanovi\u0107 D King T Reynolds A Tinelli C (2011) Cvc4. In: Proceedings of the 23rd international conference on computer aided verification CAV'11. Springer Berlin pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Berdine J. Calcagno C. OHearn PW : A decidable fragment of separation logic. In: Lodaya K. Mahajan M. (eds.) FSTTCS 2004: foundations of software technology and theoretical computer science. Lecture Notes in Computer Science vol. 3328 pp. 97\u2013109. Springer Berlin (2004)","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Berdine J Calcagno C O'Hearn PW (2006) Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of the 4th international conference on formal methods for components and objects FMCO'05. Springer Berlin pp 115\u2013137","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Berdine J Calcagno C O'Hearn PW Mary Q (2005) Symbolic execution with separation logic. In: In APLAS. Springer pp 52\u201368","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_2_6_2","unstructured":"Bao Y Ernst G (2016) A KIV project for defining semantics for intuitionistic separation logic. http:\/\/www.eecs.ucf.edu\/~ybao\/project\/sl-semantics\/index.xml"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bao Y Ernst G (2016) A KIV project for proving encoding supported separation logic into unified fine-grained region logic. http:\/\/www.eecs.ucf.edu\/~ybao\/project\/frl-sep-expr\/index.xml","DOI":"10.1145\/2786536.2786537"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-34281-3_14","volume-title":"Formal methods and software engineering: 14th international conference on formal engineering methods, ICFEM 2012, Kyoto, Japan, November 12\u201316 proceedings","author":"Bobot B","year":"2012"},{"key":"e_1_2_1_2_9_2","volume-title":"Verification of object-oriented software: the KeY approach Lecture Notes in Computer Science","author":"Beckert B","year":"2007"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bao Y Leavens GT Ernst G (2015) Conditional effects in fine-grained region logic. In: Proceedings of the 17th Workshop on formal techniques for Java-like programs FTfJP '15. ACM New York NY USA pp 5:1\u20135:6","DOI":"10.1145\/2786536.2786537"},{"key":"e_1_2_1_2_11_2","unstructured":"Bao Y Leavens GT Ernst G (2016) Fine-grained region logic and unified fine-grained region logic. Technical report CS-TR-16-01 Computer Science University of Central Florida Orlando FL August 2016. http:\/\/www.eecs.ucf.edu\/~ybao\/tech-reports\/FRL-UFRL-TR.pdf"},{"key":"e_1_2_1_2_12_2","first-page":"49","volume-title":"Construction and analysis of safe, secure, and interoperable smart devices (CASSIS 2004) (Lecture Notes in Computer Science)","author":"Barnett M","year":"2005"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Banerjee B Naumann DA (2013) Local reasoning for global invariants part ii: dynamic boundaries. J ACM 60(3):19:1\u201319:73","DOI":"10.1145\/2487241.2485981"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-12154-3_1","volume-title":"Verified software: theories, tools and experiments: 6th international conference, VSTTE 2014, Vienna, Austria, July 17\u201318, revised selected papers","author":"Banerjee A","year":"2014"},{"key":"e_1_2_1_2_16_2","first-page":"387","volume-title":"European conference on object-oriented programming (ECOOP) (Lecture Notes in Computer Science)","author":"Banerjee A","year":"2008"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Banerjee A Naumann DA Rosenberg S (2013) Local reasoning for global invariants part i: region logic. J ACM 60(3):18:1\u201318:56","DOI":"10.1145\/2487241.2485982"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Brotherston J (2007) Formalised inductive reasoning in the logic of bunched implications. In: Proceedings of the 14th international conference on static analysis SAS'07. Springer Berlin pp 87\u2013103","DOI":"10.1007\/978-3-540-74061-2_6"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Cook B Haase C Ouaknine J Parkinson M Worrell J (2011) Tractable reasoning in a fragment of separation logic. In: CONCUR 2011\u2013Concurrency theory: 22nd international conference CONCUR 2011 Aachen Germany September 6\u20139 2011. Proceedings. Springer Berlin pp 235\u2013249","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"e_1_2_1_2_20_2","first-page":"342","volume-title":"Formal methods for components and objects (FMCO) 2005, Revised Lectures (Lecture Notes in Computer Science)","author":"Chalin P","year":"2006"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.649"},{"key":"e_1_2_1_2_22_2","first-page":"337","volume-title":"Tools and algorithms for the construction and analysis (TACAS) (Lecture Notes in Computer Science)","author":"de Moura L","year":"2008"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Distefano D O'Hearn PW Yang H (2006) A local shape analysis based on separation logic. In Proceedings of the 12th International conference on tools and algorithms for the construction and analysis of systems TACAS'06. Springer Berlin pp 287\u2013302","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Ernst G Pfhler J Schellhorn G Haneberg D Reif W (2014) Kiv: overview and verifythis competition. Int J Softw Tools Technol Transf 1\u201318","DOI":"10.1007\/s10009-014-0308-3"},{"key":"e_1_2_1_2_25_2","unstructured":"Ford RL Leino KRM (2017) Dafny reference manual (draft). https:\/\/github.com\/Microsoft\/dafny\/blob\/master\/Docs\/DafnyRef\/out\/DafnyRef.pdf"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.231756"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hobor A Villard J (2012) The ramifications of sharing in data structures. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL '13. ACM New York pp 523\u2013536","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Ishtiaq SS O'Hearn PW (2001) BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL '01. ACM New York pp 14\u201326","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/16173"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Jacobs B Smans J Piessens F (2010) The verifast program verifier: a tutorial","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"e_1_2_1_2_31_2","first-page":"268","volume-title":"Formal methods (FM) (Lecture Notes in Computer Science)","author":"Kassios IT","year":"2006"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_2_1_2_33_2","unstructured":"Leavens GT Baker AL Ruby C (2001) Preliminary design of JML: a behavioral interface specification language for Java. Technical Report 98-06q Iowa State University Department of Computer Science December 2001. This is an obsolete version"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_35_2","unstructured":"Leino KRM (1995) Toward reliable modular programs. Ph.D. thesis California Institute of Technology. Available as Technical Report Caltech-CS-TR-95-03"},{"key":"e_1_2_1_2_36_2","first-page":"144","volume-title":"OOPSLA '98 conference proceedings (ACM SIGPLAN Notices), vol 33(10)","author":"Leino KRM","year":"1998"},{"key":"e_1_2_1_2_37_2","unstructured":"Leino KRM (2008) Specification and verification of object-oriented software. Lecture notes from Marktoberdorf Internation Summer School. http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml190.pdf"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Logic for programming artificial intelligence and reasoning 16th international conference LPAR-16 (Lecture Notes in Computer Science) vol 6355. Springer pp 348\u2013370","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_2_39_2","first-page":"378","volume-title":"Programming languages and systems, 18th European symposium on programming, ESOP 2009 (Lecture Notes in Computer Science)","author":"Leino KRM","year":"2009"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Monahan R (2010) Dafny meets the verification benchmarks challenge. In: Proceedings of the third international conference on verified software: theories tools experiments (Lecture Notes in Computer Science) vol 6217. Springer Berlin pp 112\u2013126","DOI":"10.1007\/978-3-642-15057-9_8"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Leino KRM Poetzsch-Heffter A Zhou Y (2002) Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN 2002 Conference on programming language design and implementation (PLDI'02) (ACM SIGPLAN Notices) vol 37(5). ACM New York pp 246\u2013257","DOI":"10.1145\/543552.512559"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Mostowski W Ulbrich M (2015) Dynamic dispatch for method contracts through abstract predicates. In: Proceedings of the 14th international conference on modularity MODULARITY 2015. ACM New York pp 109\u2013116","DOI":"10.1145\/2724525.2724574"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/1767748"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Noble J Vitek J Potter J (1998) Flexible alias protection. In: Jul E (ed) ECOOP '98\u2014Object-oriented programming 12th European conference Brussels Belgium (Lecture Notes in Computer Science) vol 1445. Springer pp 158\u2013185","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"O'Hearn P Reynolds J Yang H (2001) Local reasoning about programs that alter data structures. In: Proceedings of CSL'01 (Lecture Notes in Computer Science) vol 2142. Springer Berlin pp 1\u201319","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"O'Hearn PW Yang H Reynolds JC (2004) Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL '04. ACM New York pp 268\u2013280","DOI":"10.1145\/964001.964024"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"O'Hearn PW Yang H Reynolds JC (2009) Separation and information hiding. ACM Trans Program Lang Syst 31(3):11:1\u201311:50","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_2_50_2","unstructured":"Parkinson MJ (2005) Local reasoning for Java. Technical Report 654 University of Cambridge Computer Laboratory November 2005. The author's Ph.D. dissertation"},{"key":"e_1_2_1_2_51_2","first-page":"247","volume-title":"ACM symposium on principles of programming languages","author":"Parkinson M","year":"2005"},{"key":"e_1_2_1_2_52_2","first-page":"75","volume-title":"ACM symposium on principles of programming languages","author":"Parkinson M","year":"2008"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Parkinson M.J. Summers A.J.: The relationship between separation logic and implicit dynamic frames. Log Methods Comput Sci 8 (3) (2012)","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-642-27940-9_25","volume-title":"Verification, Model checking, and abstract interpretation","author":"Rosenberg S","year":"2012"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of the seventeenth annual IEEE symposium on logic in computer science. IEEE Computer Society Press Los Alamitos pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Smans J Jacobs B Piessens F (2010) Heap-dependent expressions in separation logic. In: Proceedings of the 12th IFIP WG 6.1 international conference and 30th IFIP WG 6.1 international conference on formal techniques for distributed systems FMOODS'10\/FORTE'10. Springer Berlin pp 170\u2013185","DOI":"10.1007\/978-3-642-13464-7_14"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Smans J Jacobs B Piessens F (2012) Implicit dynamic frames. ACM Trans Program Lang Syst 34(1):2:1\u20132:58","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0148-1"},{"key":"e_1_2_1_2_59_2","unstructured":"Tuerk T (2010) Local reasoning about while-loops. In: International conference on verified software: theories tools and experiments\u2014theory workshop (VS-Theory"},{"key":"e_1_2_1_2_60_2","unstructured":"Wei\u00df B (2011) Deductive Verification of object-oriented software: dynamic frames dynamic logic and predicate abstraction. Ph.D. thesis Karlsruhe Institute of Technology"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Yang H O'Hearn PW (2002) A semantic basis for local reasoning. In: Proceedings of the 5th international conference on foundations of software science and computation structures FoSSaCS '02. Springer London pp 402\u2013416","DOI":"10.1007\/3-540-45931-6_28"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0455-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0455-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0455-5","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0455-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0455-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T20:28:36Z","timestamp":1693686516000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0455-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8]]},"references-count":61,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["10.1007\/s00165-018-0455-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0455-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8]]},"assertion":[{"value":"21 January 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}