{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T09:02:15Z","timestamp":1788080535159,"version":"build-2784847793"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001459","name":"Singapore Ministry of Education","doi-asserted-by":"crossref","award":["MOE-MOET32021-0001"],"award-info":[{"award-number":["MOE-MOET32021-0001"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    We present an approach to automatically synthesise recursive predicates in Separation Logic (SL) from concrete data structure instances using Inductive Logic Programming (ILP) techniques. The main challenges to make such synthesis effective are (1) making it work without negative examples that are required in ILP but are difficult to construct for heap-based structures in an automated fashion, and (2) to be capable of summarising not just the\n                    <jats:italic toggle=\"yes\">shape<\/jats:italic>\n                    of a heap\n                    <jats:italic toggle=\"yes\">(e.g.,<\/jats:italic>\n                    it is a\n                    <jats:italic toggle=\"yes\">linked<\/jats:italic>\n                    list), but also the\n                    <jats:italic toggle=\"yes\">properties<\/jats:italic>\n                    of the data it stores\n                    <jats:italic toggle=\"yes\">(e.g.,<\/jats:italic>\n                    it is a\n                    <jats:italic toggle=\"yes\">sorted<\/jats:italic>\n                    linked list). We tackle these challenges with a new predicate learning algorithm. The key contributions of our work are (a) the formulation of ILP-based learning only using positive examples and (b) an algorithm that synthesises property-rich SL predicates from concrete\n                    <jats:italic toggle=\"yes\">memory graphs<\/jats:italic>\n                    based on the positive-only learning.\n                  <\/jats:p>\n                  <jats:p>We show that our framework can efficiently and correctly synthesise SL predicates for structures that were beyond the reach of the state-of-the-art tools, including those featuring non-trivial payload constraints (e.g., binary search trees) and nested recursion (e.g., n-ary trees). We further extend the usability of our approach by a memory graph generator that produces positive heap examples from programs. Finally, we show how our approach facilitates deductive verification and synthesis of correct-by-construction code.<\/jats:p>","DOI":"10.1145\/3720420","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"169-195","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Inductive Synthesis of Inductive Heap Predicates"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8015-7846","authenticated-orcid":false,"given":"Ziyi","family":"Yang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485481"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571200"},{"key":"e_1_3_1_7_2","unstructured":"Nikolaj Bj\u00f8rner Clemens Eisenhofer and Laura Kov\u00e1cs. 2022. User-Propagation for Custom Theories in SMT Solving. In Satisfiability Modulo Theories. 20th International Workshop."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23264-5_13"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Jan H. Boockmann and Gerald Luettgen. 2020. Learning Data Structure Shapes from Memory Graphs. In LPAR (EPiC Series in Computing Vol. 73). EasyChair 151\u2013168. https:\/\/doi.org\/10.29007\/dhpw 10.29007\/dhpw","DOI":"10.29007\/dhpw"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3524610.3527913"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_4"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31951-8_12"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V36I6.20596"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Andrew Cropper and Sebastijan Dumancic. 2022. Inductive Logic Programming At 30: A New Introduction. J. Artif. Intell. Res. 74 (2022) 765\u2013850. https:\/\/doi.org\/10.1613\/JAIR.1.13507 10.1613\/JAIR.1.13507","DOI":"10.1613\/JAIR.1.13507"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-021-06089-1"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Andrew Cropper Sebastijan Dumancic and Stephen H. Muggleton. 2020. Turning 30: New Ideas in Inductive Logic Programming. (2020) 4833\u20134839. https:\/\/doi.org\/10.24963\/IJCAI.2020\/673 10.24963\/IJCAI.2020\/673","DOI":"10.24963\/IJCAI.2020\/673"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-020-05934-z"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23708-4_5"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Dohrau. 2022. Automatic Inference of Permission Specifications. Ph.D. Dissertation. ETH Zurich Z\u00fcrich Switzerland. https:\/\/doi.org\/10.3929\/ETHZ-B-000588977 10.3929\/ETHZ-B-000588977","DOI":"10.3929\/ETHZ-B-000588977"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2488388.2488425"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.2200\/S00457ED1V01Y201211AIM019"},{"key":"e_1_3_1_25_2","unstructured":"Martin Gebser Roland Kaminski Benjamin Kaufmann and Torsten Schaub. 2014. Clingo = ASP + Control: Preliminary Report. CoRR abs\/1405.3694 (2014). arXiv:1405.3694 http:\/\/arxiv.org\/abs\/1405.3694"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000054"},{"key":"e_1_3_1_27_2","first-page":"1070","volume-title":"ICLP","author":"Gelfond Michael","year":"1988","unstructured":"Michael Gelfond and Vladimir Lifschitz. 1988. The Stable Model Semantics for Logic Programming. In ICLP. MIT Press, 1070\u20131080."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(93)90062-G"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068417000242"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485544"},{"key":"e_1_3_1_34_2","first-page":"569","volume-title":"Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974","author":"Kowalski Robert A.","year":"1974","unstructured":"Robert A. Kowalski. 1974. Predicate Logic as Programming Language. In Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974, Jack L. Rosenfeld (Ed.). North-Holland, 569\u2013574."},{"key":"e_1_3_1_35_2","unstructured":"Michael Langowski. 2022. ASP - A Tutorial. https:\/\/madmike200590.github.io\/asp-guide\/tutorial.html"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V34I03.5678"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11558-0_22"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314634"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Lezhi Ma Shangqing Liu Yi Li Xiaofei Xie and Lei Bu. 2024. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. CoRR abs\/2401.08807 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.08807 10.48550\/ARXIV.2401.08807","DOI":"10.48550\/ARXIV.2401.08807"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.69"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00084"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00112"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622876"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037089"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037227"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63494-0_65"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-013-5358-3"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_17"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_17"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"issue":"1","key":"e_1_3_1_56_2","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin Gordon D","year":"1970","unstructured":"Gordon D Plotkin. 1970. A note on inductive generalization. Machine intelligence 5, 1 (1970), 153\u2013163.","journal-title":"Machine intelligence"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_1_58_2","volume-title":"An Introduction to Separation Logic (Preliminary Draft)","author":"Reynolds John C.","year":"2008","unstructured":"John C. Reynolds. 2008. An Introduction to Separation Logic (Preliminary Draft). Technical Report. Carnegie Mellon University."},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_9"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236034"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_8"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_58"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454098"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622847"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30923-7_13"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180250"},{"key":"e_1_3_1_67_2","volume-title":"Stuctural properties and minimization of Horn Boolean functions","author":"\u010cepek Ond\u0159ej","year":"1995","unstructured":"Ond\u0159ej \u010cepek. 1995. Stuctural properties and minimization of Horn Boolean functions. Ph.D. Dissertation. Rutgers University."},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473589"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"e_1_3_1_70_2","unstructured":"Ziyi Yang and Ilya Sergey. 2025. Inductive Synthesis of Inductive Heap Predicates \u2013 Extended Version. CoRR abs\/2502.14478 (2025). arXiv:2502.14478 http:\/\/arxiv.org\/abs\/2502.14478"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","unstructured":"Ziyi Yang and Ilya Sergey. 2025. Sippy: the Artefact for the Paper \u201cInductive Synthesis of Inductive Heap Predicates\u201d. https:\/\/doi.org\/10.5281\/zenodo.14928260 10.5281\/zenodo.14928260","DOI":"10.5281\/zenodo.14928260"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720420","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720420","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:38Z","timestamp":1787589098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720420"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":71,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720420"],"URL":"https:\/\/doi.org\/10.1145\/3720420","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}