{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:50Z","timestamp":1772119610041,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T00:00:00Z","timestamp":1501718400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0289-4","type":"journal-article","created":{"date-parts":[[2017,8,3]],"date-time":"2017-08-03T09:57:47Z","timestamp":1501754267000},"page":"575-607","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Compositional entailment checking for a fragment of separation logic"],"prefix":"10.1007","volume":"51","author":[{"given":"Constantin","family":"Enea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,3]]},"reference":[{"key":"289_CR1","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW, Wies T, Yang H (2007) Shape analysis for composite data structures. In: Proceedings of CAV\u201907, volume 4590 of LNCS, pp 178\u2013192. Springer","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"289_CR2","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, O\u2019Hearn PW (2005) A decidable fragment of separation logic. In: Proceedings of FSTTCS\u201904, volume 3328 of LNCS, pp 97\u2013109. Springer","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"289_CR3","doi-asserted-by":"crossref","unstructured":"Berdine J, Calcagno C, O\u2019Hearn PW (2006) Smallfoot: modular automatic assertion checking with separation logic. In: Proceedings of FMCO\u201905, volume 4111 of LNCS, pp 115\u2013137. Springer","DOI":"10.1007\/11804192_6"},{"key":"289_CR4","doi-asserted-by":"crossref","unstructured":"Brotherston J, Fuhs C, Gorogiannis N, P\u00e9rez JN (2014) A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of CSL-LICS\u201914, pp 25:1\u201325:10. ACM","DOI":"10.1145\/2603088.2603091"},{"key":"289_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston J, Gorogiannis N, Petersen RL (2012) A generic cyclic theorem prover. In: Proceedings of APLAS\u201912, volume 7705 of LNCS, pp 350\u2013367. Springer","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"289_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno C, Yang H, O\u2019Hearn PW (2001) Computability and complexity results for a spatial assertion language for data structures. In: Proceedings of FSTTCS\u201901, volume 2245 of LNCS, pp 108\u2013119. Springer","DOI":"10.1007\/3-540-45294-X_10"},{"issue":"9","key":"289_CR7","doi-asserted-by":"crossref","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin W-N, David C, Huu HN, Shengchao Q (2012) Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci Comput Program 77(9):1006\u20131036","journal-title":"Sci Comput Program"},{"key":"289_CR8","doi-asserted-by":"crossref","unstructured":"Cook B, Haase C, Ouaknine J, Parkinson MJ, Worrell J (2011) Tractable reasoning in a fragment of separation logic. In: Proceedings of CONCUR\u201911, volume 6901 of LNCS, pp 235\u2013249. Springer","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"289_CR9","doi-asserted-by":"crossref","unstructured":"Enea C, Leng\u00e1l O, Sighireanu M, Vojnar T (2014) Compositional entailment checking for a fragment of separation logic. In: Proceedings of APLAS\u201914, volume 8858 of LNCS, pp 314\u2013333. Springer","DOI":"10.1007\/978-3-319-12736-1_17"},{"key":"289_CR10","unstructured":"Enea C, Leng\u00e1l O, Sighireanu M, Vojnar T (2014) Spen. https:\/\/www.irif.fr\/~sighirea\/spen"},{"key":"289_CR11","doi-asserted-by":"crossref","unstructured":"Enea C, Saveluc V, Sighireanu M (2013) Compositional invariant checking for overlaid and nested linked lists. In: Proceedings of ESOP\u201913, volume 7792 of LNCS, pp 129\u2013148. Springer","DOI":"10.1007\/978-3-642-37036-6_9"},{"key":"289_CR12","doi-asserted-by":"crossref","unstructured":"Enea C, Sighireanu M, Wu Z (2015) On automated lemma generation for separation logic with inductive definitions. In: ATVA\u201915, volume 9364 of LNCS, pp 80\u201396. Springer","DOI":"10.1007\/978-3-319-24953-7_7"},{"key":"289_CR13","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0049-237X(08)71879-2","volume":"107","author":"H Gaifman","year":"1982","unstructured":"Gaifman H (1982) On local and non-local properties. Stud Logic Found Math 107:105\u2013135","journal-title":"Stud Logic Found Math"},{"key":"289_CR14","doi-asserted-by":"crossref","unstructured":"Gu X, Chen T, Wu Z (2016) A complete decision procedure for linearly compositional separation logic with data constraints. In: Proceedings of IJCAR\u201916, volume 9706 of LNCS, pp 532\u2013549. Springer","DOI":"10.1007\/978-3-319-40229-1_36"},{"key":"289_CR15","doi-asserted-by":"crossref","unstructured":"Iosif R, Rogalewicz A, \u0160im\u00e1\u010dek J (2013) The tree width of separation logic with recursive definitions. In: Proceedings of CADE\u201913, volume 7898 of LNCS, pp 21\u201338. Springer","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"289_CR16","doi-asserted-by":"crossref","unstructured":"Iosif R, Rogalewicz A, Vojnar T (2014) Deciding entailments in inductive separation logic with tree automata. In: Proceedings of ATVA\u201914, volume 8837 of LNCS, pp 201\u2013218. Springer","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"289_CR17","doi-asserted-by":"crossref","unstructured":"Ishtiaq S, O\u2019Hearn PW (2001) BI as an assertion language for mutable data structures. In: Proceedings of POPL\u201901, pp 14\u201326. ACM","DOI":"10.1145\/360204.375719"},{"key":"289_CR18","doi-asserted-by":"crossref","unstructured":"Le QL, Sun J, Chin W-N (2016) Satisfiability modulo heap-based programs. In: Proceedings of CAV\u201916, volume 9779 of LNCS, pp 382\u2013404. Springer","DOI":"10.1007\/978-3-319-41528-4_21"},{"key":"289_CR19","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l O, \u0160im\u00e1\u010dek J, Vojnar T (2012) Vata: a library for efficient manipulation of non-deterministic tree automata. In: Proceedings of TACAS\u201912, volume 7214 of LNCS, pp 79\u201394. Springer","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"289_CR20","doi-asserted-by":"crossref","unstructured":"P\u00e9rez JN, Rybalchenko A (2011) Separation logic + superposition calculus = heap theorem prover. In: Proceedings of PLDI\u201911, pp 556\u2013566. ACM","DOI":"10.1145\/1993316.1993563"},{"key":"289_CR21","doi-asserted-by":"crossref","unstructured":"P\u00e9rez JN, Rybalchenko A (2013) Separation logic modulo theories. In: Proceedings of APLAS\u201913, volume 8301 of LNCS, pp 90\u2013106. Springer","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"289_CR22","doi-asserted-by":"crossref","unstructured":"Piskac R, Wies T, Zufferey D (2013) Automating separation logic using SMT. In: Proceedings of CAV\u201913, volume 8044 of LNCS, pp 773\u2013789. Springer","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"289_CR23","doi-asserted-by":"crossref","unstructured":"Piskac R, Wies T, Zufferey D (2014) Automating separation logic with trees and data. In: Proceedings of CAV\u201914, volume 8559 of LNCS, pp 711\u2013728. Springer","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"289_CR24","doi-asserted-by":"crossref","unstructured":"Qiu X, Garg P, Stefanescu A, Madhusudan P (2013) Natural proofs for structure, data, and separation. In: Proceedings of PLDI\u201913, pp 231\u2013242. ACM","DOI":"10.1145\/2491956.2462169"},{"key":"289_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS\u201902, pp 55\u201374. IEEE","DOI":"10.1109\/LICS.2002.1029817"},{"key":"289_CR26","unstructured":"Sighireanu M, Cok D (2014) Report on SL-COMP\u201914. JSAT 1. http:\/\/smtcomp.sourceforge.net\/2014\/results-SLCOMP2.shtml"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0289-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0289-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0289-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T20:29:13Z","timestamp":1569961753000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0289-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,3]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["289"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0289-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,3]]}}}