{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:54Z","timestamp":1758053634333,"version":"3.44.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Separation logic (SL) is a widely used formalism for verifying programs\u00a0that manipulate dynamically allocated memory, relying on the separating conjunction <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\star $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u22c6<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> to combine disjoint heap structures.\u00a0The standard approach in SL lacks the expressive power to handle overlaid\u00a0data structures where multiple structures share some locations. We consider\u00a0a logic that extends SL with a new separating conjunction operator \n\"Image missing\", enabling the composition of heaps with shared locations that allocate distinct fields. Our fragment supports generic inductive definitions and introduces set variables to constrain the locations shared by overlapping structures. We prove that the satisfiability problem for this fragment is in <jats:sc>Nexptime<\/jats:sc>, by reducing it to the satisfiability problem in\u00a0BAPA [11], a decidable logic combining Boolean algebra\u00a0of sets and Presburger arithmetic.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_5","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:11Z","timestamp":1757887391000},"page":"80-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deciding Satisfiability for\u00a0Overlaid Symbolic Heaps"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-7000","authenticated-orcid":false,"given":"Nicolas","family":"Peltier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6504-8336","authenticated-orcid":false,"given":"Quentin","family":"Petitjean","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1925-089X","authenticated-orcid":false,"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_5","DOI":"10.1007\/11575467_5"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Brotherston, J., Fuhs, C., P\u00e9rez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 1\u201310. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2603088.2603091","DOI":"10.1145\/2603088.2603091"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Dr\u0103goi, C., Enea, C., Sighireanu, M.: Local shape analysis for overlaid data structures. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 150\u2013171. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_10","DOI":"10.1007\/978-3-642-38856-9_10"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Decidable entailments in separation logic with inductive definitions: beyond establishment. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 183, pp. 20:1\u201320:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.20","DOI":"10.4230\/LIPIcs.CSL.2021.20"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2021.106169","volume":"173","author":"M Echenim","year":"2022","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Entailment is undecidable for symbolic heap separation logic formul\u00e6 with non-established inductive rules. Inf. Process. Lett. 173, 106169 (2022). https:\/\/doi.org\/10.1016\/j.ipl.2021.106169","journal-title":"Inf. Process. Lett."},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 129\u2013148. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_9","DOI":"10.1007\/978-3-642-37036-6_9"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532\u2013549. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_36","DOI":"10.1007\/978-3-319-40229-1_36"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21\u201338. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_2","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 14\u201326. Association for Computing Machinery, New York (2001). https:\/\/doi.org\/10.1145\/360204.375719","DOI":"10.1145\/360204.375719"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Krishna, S., Shasha, D., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang. 2(POPL), 37:1\u201337:31 (2017). https:\/\/doi.org\/10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 260\u2013277. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_20","DOI":"10.1007\/11532231_20"},{"issue":"3","key":"5_CR12","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean algebra with presburger arithmetic. J. Autom. Reason. 36(3), 213\u2013239 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9042-1","journal-title":"J. Autom. Reason."},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215\u2013230. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_15","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Le, Q.L., Le, X.B.D.: An efficient cyclic entailment procedure in a fragment of separation logic. In: Kupferman, O., Sobocinski, P. (eds.) FoSSaCS 2023. LNCS, vol. 13992, pp. 477\u2013497. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30829-1_23","DOI":"10.1007\/978-3-031-30829-1_23"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Lee, O., Yang, H., Petersen, R.: Program analysis for overlaid data structures. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 592\u2013608. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_48","DOI":"10.1007\/978-3-642-22110-1_48"},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10703-012-0151-7","volume":"41","author":"O Lee","year":"2012","unstructured":"Lee, O., Yang, H., Petersen, R.: A divide-and-conquer approach for analysing overlaid data structures. Formal Methods Syst. Des. 41(1), 4\u201324 (2012). https:\/\/doi.org\/10.1007\/s10703-012-0151-7","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Matheja, C., Pagel, J., Zuleger, F.: A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Logic 24(1), 1:1\u20131:76 (2023). https:\/\/doi.org\/10.1145\/3534927","DOI":"10.1145\/3534927"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Meyer, R., Wies, T., Wolff, S.: Make flows small again: revisiting the flow framework. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 628\u2013646. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_32","DOI":"10.1007\/978-3-031-30823-9_32"},{"issue":"4","key":"5_CR19","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"RJ Parikh","year":"1966","unstructured":"Parikh, R.J.: On context-free languages. J. ACM 13(4), 570\u2013581 (1966). https:\/\/doi.org\/10.1145\/321356.321364","journal-title":"J. ACM"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Peltier, N.: Testing the satisfiability of formulas in separation logic with permissions. In: Ramanayake, R., Urban, J. (eds.) TABLEAUX 2023. LNCS, vol. 14278, pp. 427\u2013445. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_23","DOI":"10.1007\/978-3-031-43513-3_23"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, pp. 55\u201374 (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817. ISSN 1043-6871","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"5_CR22","doi-asserted-by":"publisher","first-page":"97","DOI":"10.3233\/FI-2013-802","volume":"123","author":"Z Sawa","year":"2013","unstructured":"Sawa, Z.: Efficient construction of semilinear representations of languages accepted by unary nondeterministic finite automata. Fundamenta Informaticae 123(1), 97\u2013106 (2013). https:\/\/doi.org\/10.3233\/FI-2013-802","journal-title":"Fundamenta Informaticae"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337\u2013352. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_25","DOI":"10.1007\/11532231_25"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:12Z","timestamp":1757887392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}