{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:54:04Z","timestamp":1767920044141,"version":"3.49.0"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["59102-SVIS"],"award-info":[{"award-number":["59102-SVIS"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["2117\/23"],"award-info":[{"award-number":["2117\/23"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>For over two decades Separation Logic has enjoyed  \nits unique position as arguably the most popular framework  \nfor reasoning about heap-manipulating programs,  \nas well as reasoning about shared resources and permissions.  \nSeparation Logic is often extended to include  \ninductively-defined predicates,  \ninterpreted as least fixpoints,  \nto form what is known as Separation Logic with Inductive Definitions (SLID).  \nThese inductive predicates are  \nused to describe unbounded data-structures in the heap  \nand to verify key properties thereof.  \nMany theoretical and practical advances  \nhave been made in developing automated proof mechanisms  \nfor SLID,  \nbut by their very nature these mechanisms are imperfect,  \nand a deeper understanding of their failures  \nis desired.  \nAs expressive as Separation Logic is, it is not surprising  \nthat it is incomplete:  \nthere is no procedure that will provide a proof  \nfor all valid entailments in Separation Logic.  \nIn fact, at its very core, Separation Logic contains several  \nsources of incompleteness that defy automated reasoning.<\/jats:p>\n                  <jats:p>In this paper we study these sources of incompleteness  \nand how they relate to failures of proof mechanisms of SLID.  \nWe contextualize SLID within a larger, relaxed logic,  \nthat we call Weak Separation Logic (WSL).  \nWe prove that unlike SLID, WSL enjoys completeness  \nfor a non-trivial  \nfragment of quantified entailments with background theories and  \ninductive definitions,  \nvia a reduction to first-order logic (FOL).  \nMoreover, we show that the ubiquitous fold\/unfold proof mechanism,  \nwhich is unsurprisingly incomplete for SLID,  \ndoes constitute a sound and complete proof mechanism of  \nWSL,  \nfor theory-free, quantifier-free entailments with inductive definitions.  \nIn some sense, this shows that WSL is the natural logic  \nof such proof mechanisms.  \nThrough this contextualization of SLID within WSL,  \nwe understand proof failures as stemming from  \nrogue, nonstandard models,  \nthat exist within the class of models considered by WSL,  \nbut do not adhere to the stricter requirements of SLID.  \nThese rogue models are typically infinite,  \nand we use the  \nrecently proposed formalism of symbolic structures  \nto represent and automatically find them.<\/jats:p>\n                  <jats:p>We present a prototype tool that implements the encoding of  \nWSL to FOL and test it on an existing benchmark,  \nwhich contains over 700  \nquantified entailment problems with inductive definitions,  \na third of which also contain background theories.  \nOur tool is able to find counter-models  \nto many of the examples,  \nand we provide a partial taxonomy of the rogue models,  \nshedding some light on real-world proof failures.<\/jats:p>","DOI":"10.1145\/3776671","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"833-864","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5503-5791","authenticated-orcid":false,"given":"Neta","family":"Elad","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09099-3_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_10"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_14"},{"key":"e_1_2_1_11_1","volume-title":"Boyer and J Strother Moore","author":"Robert","year":"1998","unstructured":"Robert S. Boyer and J Strother Moore. 1998. A computational logic handbook, Second Edition. Academic Press. isbn:978-0-12-122955-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_27"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.17"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737984"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2015.1018801"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_18"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Adithya Murali and Sharon Shoham. 2025. Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions. arXiv:2511.20193. https:\/\/doi.org\/10.48550\/arXiv.2511.20193 10.48550\/arXiv.2511.20193","DOI":"10.48550\/arXiv.2511.20193"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Adithya Murali and Sharon Shoham. 2025. Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17472710 10.5281\/zenodo.17472710","DOI":"10.5281\/zenodo.17472710"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Adithya Murali and Sharon Shoham. 2025. Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17273238 10.5281\/zenodo.17273238","DOI":"10.5281\/zenodo.17273238"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632875"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704853"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_7"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210045"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.021"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_19"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_9"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_8"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720447"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622835"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583057"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification Tobias Nipkow Orna Grumberg and Benedikt Hauptmann (Eds.) (NATO Science for Peace and Security Series - D: Information and Communication Security Vol. 33). IOS Press 286\u2013318. https:\/\/doi.org\/10.3233\/978-1-61499-028-4-286 10.3233\/978-1-61499-028-4-286","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_2_1_59_1","unstructured":"Jens Pagel. 2020. Decision procedures for separation logic: beyond symbolic heaps. Ph. D. Dissertation. Technische Universit\u00e4t Wien."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00628-w"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190107"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244275"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158097"},{"key":"e_1_2_1_79_1","doi-asserted-by":"crossref","unstructured":"Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications..","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/1593511"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776671","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:17Z","timestamp":1767898997000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776671"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":82,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776671"],"URL":"https:\/\/doi.org\/10.1145\/3776671","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}