{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:03Z","timestamp":1776305283601,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572456","type":"print"},{"value":"9783031572463","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. Our method is based on a model-based translation to SMT for which we introduce several optimisations\u2014the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. Through a series of experiments, we show that, on the frequently used symbolic heap fragment, our decision procedure is competitive with other existing approaches, and it can outperform them outside the symbolic heap fragment. Moreover, our decision procedure can also handle some formulae for which no decision procedure has been implemented so far.<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_11","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"188-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Deciding Boolean Separation Logic via Small Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4083-8943","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Dac\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7911-0549","authenticated-orcid":false,"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2746-8792","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bansal, K., Barrett, C., Reynolds, A., Tinelli, C.: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. In: IJCAR (2017)","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Batz, K., Fesefeldt, I., Jansen, M., Katoen, J.P., Ke\u00dfler, F., Matheja, C., Noll, T.: Foundations for Entailment Checking in Quantitative Separation Logic. In: ESOP (2022)","DOI":"10.1007\/978-3-030-99336-8_3"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A Decidable Fragment of Separation Logic. In: FSTTCS 2004. LNCS, vol.\u00a03328 (2004)","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer 21 (2017)","DOI":"10.1007\/s10009-017-0469-y"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A Generic Cyclic Theorem Prover. In: APLAS. LNCS, vol.\u00a07705 (2012)","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional Shape Analysis by Means of Bi-Abduction. Journal of the ACM 58(6) (2011)","DOI":"10.1145\/2049697.2049700"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: FST TCS (2001)","DOI":"10.1007\/3-540-45294-X_10"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable Reasoning in a Fragment of Separation Logic. In: CONCUR. LNCS, vol.\u00a03901 (2011)","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"11_CR9","unstructured":"Dac\u00edk, T., Rogalewicz, A., Vojnar, T., Zuleger, F.: Deciding Boolean Separation Logic via Small Models. Tech. rep. (10 2023), https:\/\/zenodo.org\/records\/10012893"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: The Bernays-Sch\u00f6nfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Transactions on Computational Logic 21 (2019)","DOI":"10.1145\/3380809"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Enea, C., Leng\u00e1l, O., Sighireanu, M., Vojnar, T.: Compositional Entailment Checking for a Fragment of Separation Logic. In: APLAS (2014)","DOI":"10.1007\/978-3-319-12736-1_17"},{"key":"11_CR12","unstructured":"Hol\u00edk, L., Peringer, P., Rogalewicz, A., \u0160okov\u00e1, V., Vojnar, T., Zuleger, F.: Low-level bi-abduction. In: ECOOP 2022. LIPIcs, vol.\u00a0222, pp. 19:1\u201319:30 (2022)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding Entailments in Inductive Separation Logic with Tree Automata. In: ATVA (2014)","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Iosif, R., Zuleger, F.: Expressiveness results for an inductive logic of separated relations. In: P\u00e9rez, G.A., Raskin, J. (eds.) CONCUR. LIPIcs, vol.\u00a0279, pp. 20:1\u201320:20 (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.20, https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2023.20","DOI":"10.4230\/LIPICS.CONCUR.2023.20 10.4230\/LIPIcs.CONCUR.2023.20"},{"key":"11_CR15","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: Separation and Information Hiding. In: Proc. of POPL\u201901. ACM (2001)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Katelaan, J., Jovanovic, D., Weissenbacher, G.: A Separation Logic with Data: Small Models and Automation. In: IJCAR (2018)","DOI":"10.1007\/978-3-319-94205-6_30"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Katelaan, J., Matheja, C., Noll, T., Zuleger, F.: Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic. In: LPAR-22 Workshop and Short Paper Proceedings. vol.\u00a09 (2018)","DOI":"10.29007\/qwd8"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.N.: Shape Analysis via Second-Order Bi-Abduction. In: Proc. of CAV\u201914. LNCS, vol.\u00a08559. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Le, Q.L.: Compositional Satisfiability Solving in Separation Logic. In: VMCAI. LNCS, vol. 12597 (2021)","DOI":"10.1007\/978-3-030-67067-2_26"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Le, X.B.D.: An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic. In: FoSSaCS (2023)","DOI":"10.1007\/978-3-031-30829-1_23"},{"key":"11_CR21","doi-asserted-by":"crossref","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) (2023)","DOI":"10.1145\/3534927"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Navarro\u00a0P\u00e9rez, J.A., Rybalchenko, A.: Separation Logic + Superposition Calculus = Heap Theorem Prover. In: PLDI (2011)","DOI":"10.1145\/1993498.1993563"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Navarro\u00a0P\u00e9rez, J.A., Rybalchenko, A.: Separation Logic Modulo Theories. In: APLAS. LNCS, vol.\u00a08301 (2013)","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: CAV. LNCS, vol. 13965 (2023)","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Pagel, J., Zuleger, F.: Strong-separation logic. ACM Trans. Program. Lang. Syst. 44(3), 16:1\u201316:40 (2022). https:\/\/doi.org\/10.1145\/3498847, https:\/\/doi.org\/10.1145\/3498847","DOI":"10.1145\/3498847 10.1145\/3498847"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic Using SMT. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic with Trees and Data. In: CAV (2014)","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., King, T.: A Decision Procedure for Separation Logic in SMT. In: ATVA (2016)","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"11_CR30","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science (2002)"},{"key":"11_CR31","unstructured":"Santos, J., Maksimovic, P., Ayoun, S.E., Gardner, P.: Gillian, Part I: A Multi-Language Platform for Symbolic Execution. In: Proc. of PLDI\u201920. ACM (2020)"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Summers, A.J., M\u00fcller, P.: Automating deductive verification for weak-memory programs (extended version). Int. J. Softw. Tools Technol. Transf. 22(6), 709\u2013728 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00559-y","DOI":"10.1007\/s10009-020-00559-y"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Ta, Q.T., Le, T.C., Khoo, S.C., Chin, W.N.: Automated Lemma Synthesis in Symbolic-Heap Separation Logic. In: POPL (2018)","DOI":"10.1145\/3158097"},{"key":"11_CR34","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.: Scalable Shape Analysis for Systems Code. In: Proc. of CAV\u201908. LNCS, vol.\u00a05123. Springer (2008)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T16:14:50Z","timestamp":1731687290000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}