{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:34:32Z","timestamp":1770280472056,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.<\/jats:p>","DOI":"10.1145\/3563354","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1873-1902","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Model-guided synthesis of inductive lemmas for FOL with least fixpoints"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1898-439X","authenticated-orcid":false,"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8270-8226","authenticated-orcid":false,"given":"Eion","family":"Blanchard","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1529-2806","authenticated-orcid":false,"given":"Christof","family":"L\u00f6ding","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"#cr-split#-e_1_2_1_4_1.1","unstructured":"Kshitij Bansal Sarah M. Loos Markus N. Rabe Christian Szegedy and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving. https:\/\/doi.org\/10.48550\/ARXIV.1904.03241 10.48550\/ARXIV.1904.03241"},{"key":"#cr-split#-e_1_2_1_4_1.2","unstructured":"Kshitij Bansal Sarah M. Loos Markus N. Rabe Christian Szegedy and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving. https:\/\/doi.org\/10.48550\/ARXIV.1904.03241"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_6_1","volume-title":"A Computational Logic Handbook","author":"Boyer Robert S.","unstructured":"Robert S. Boyer and J. Strother Moore . 1988. A Computational Logic Handbook . Academic Press Professional, Inc. , USA. isbn:0121229521 Robert S. Boyer and J. Strother Moore. 1988. A Computational Logic Handbook. Academic Press Professional, Inc., USA. isbn:0121229521"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_25"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737984"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_10"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-0-22107-6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498722"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68804-8"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"e_1_2_1_22_1","volume-title":"A Shorter Model Theory","author":"Hodges Wilfrid","unstructured":"Wilfrid Hodges . 1997. A Shorter Model Theory . Cambridge University Press , USA. isbn:0521587131 Wilfrid Hodges. 1997. A Shorter Model Theory. Cambridge University Press, USA. isbn:0521587131"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-23250-4_9"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009887"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498671"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_2_1_35_1","first-page":"729","article-title":"Axiomatizable classes of locally free algebras of certain types","volume":"3","author":"Mal\u2019tsev A. I.","year":"1962","unstructured":"A. I. Mal\u2019tsev . 1962 . Axiomatizable classes of locally free algebras of certain types . Sibirsk. Mat. Zh. , 3 (1962), 729 \u2013 743 . http:\/\/mi.mathnet.ru\/eng\/smj\/v3\/i5\/p729 A. I. Mal\u2019tsev. 1962. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Zh., 3 (1962), 729\u2013743. http:\/\/mi.mathnet.ru\/eng\/smj\/v3\/i5\/p729","journal-title":"Sibirsk. Mat. Zh."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554331"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_19"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_33"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_13"},{"key":"e_1_2_1_40_1","volume-title":"Techniques for Program Verification. Ph. D. Dissertation","author":"Nelson Charles Gregory","unstructured":"Charles Gregory Nelson . 1980. Techniques for Program Verification. Ph. D. Dissertation . Stanford University . Stanford, CA, USA. AAI8011683 Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph. D. Dissertation. Stanford University. Stanford, CA, USA. AAI8011683"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.29007\/jmd3"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_28"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_8"},{"key":"e_1_2_1_52_1","volume-title":"Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department","author":"Lezama Armando Solar","year":"2008","unstructured":"Armando Solar Lezama . 2008. Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department , University of California , Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/ 2008 \/EECS-2008-177.html Armando Solar Lezama. 2008. Program Synthesis By Sketching. Ph. D. Dissertation. EECS Department, University of California, Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2008\/EECS-2008-177.html"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158097"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_35"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_15"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563354","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563354","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:33Z","timestamp":1750186953000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563354"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":61,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563354"],"URL":"https:\/\/doi.org\/10.1145\/3563354","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}