{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T04:29:10Z","timestamp":1779078550146,"version":"3.51.4"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>\n            Loop invariant inference is a fundamental, yet challenging, problem in program verification. Recent work adopts the\n            <jats:italic toggle=\"yes\">guess-and-check<\/jats:italic>\n            framework, where candidate loop invariants are iteratively generated in the\n            <jats:italic toggle=\"yes\">guess<\/jats:italic>\n            step and verified in the\n            <jats:italic toggle=\"yes\">check<\/jats:italic>\n            step. A major challenge of this general framework is to produce high-quality candidate invariants in each iteration so that the inference procedure can converge quickly. Empirically, we observe that existing approaches may struggle with guessing the complete invariant due to the complexity of logical connectives, but usually, all the\n            <jats:italic toggle=\"yes\">clauses<\/jats:italic>\n            of the correct loop invariant have already appeared in the previous guesses. This motivates us to refine the guess-and-check framework, resulting in a\n            <jats:italic toggle=\"yes\">generate-combine-check<\/jats:italic>\n            framework, where the loop invariant inference task is divided into clause generation and clause combination. Specifically, we propose a novel loop invariant inference approach under the new framework, which consists of an LLM-based clause generator and a counterexample-driven clause combinator. As the clause generator, leverages LLMs to generate a multitude of clauses; as the clause combinator, leverages counterexamples from the previous rounds to convert generated clauses into invariants. Our experiments show that significantly outperforms existing loop invariant inference approaches. For example, solved 312 (out of 316) linear invariant inference tasks and 44 (out of 50) nonlinear invariant inference tasks, which is at least 93 and 16 more than the existing baselines, respectively. By design, the\n            <jats:italic toggle=\"yes\">generate-combine-check<\/jats:italic>\n            framework is flexible to accommodate various existing approaches which are currently under the\n            <jats:italic toggle=\"yes\">guess-and-check<\/jats:italic>\n            framework by splitting the guessed candidate invariants into clauses. The evaluation shows that our approach can, with minor adaptation, improve existing loop invariant inference approaches in both effectiveness and efficiency. For example, Code2Inv which solved 210 linear problems with an average solving time of 137.6 seconds can be improved to solve 252 problems with an average solving time of 17.8 seconds.\n          <\/jats:p>","DOI":"10.1145\/3728920","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"1009-1030","source":"Crossref","is-referenced-by-count":3,"title":["Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2433-4920","authenticated-orcid":false,"given":"Weining","family":"Cao","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4689-4097","authenticated-orcid":false,"given":"Guangyuan","family":"Wu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0438-5299","authenticated-orcid":false,"given":"Tangzhi","family":"Xu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6913-6542","authenticated-orcid":false,"given":"Yuan","family":"Yao","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0427-9710","authenticated-orcid":false,"given":"Hengfeng","family":"Wei","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5993-1665","authenticated-orcid":false,"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[{"name":"Birkbeck University of London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7970-1384","authenticated-orcid":false,"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"SyGuS-Comp 2018: Results and Analysis. CoRR abs\/1904.07146","author":"Alur Rajeev","year":"2019","unstructured":"Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa. 2019. SyGuS-Comp 2018: Results and Analysis. CoRR abs\/1904.07146 (2019). arXiv preprint arXiv:1904.07146."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPRIME.2012.6208380"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.5477"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional recurrence analysis. In 2015 Formal Methods in Computer-Aided Design (FMCAD). 57\u201364. https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253 10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/279943.279985"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The ELDARICA Horn Solver. In 2018 Formal Methods in Computer Aided Design (FMCAD). 1\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013 10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_1_25_1","unstructured":"Adharsh Kamath Aditya Senthilnathan Saikat Chakraborty Pantazis Deligiannis Shuvendu K Lahiri Akash Lal Aseem Rastogi Subhajit Roy and Rahul Sharma. 2023. Finding Inductive Loop Invariants using Large Language Models. arXiv preprint arXiv:2311.07948."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115689"},{"key":"e_1_2_1_29_1","volume-title":"The Eleventh International Conference on Learning Representations (ICLR).","author":"Li Zenan","year":"2023","unstructured":"Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, and Jian L\u00fc. 2023. Learning with Logical Constraints but without Shortcut Satisfaction. In The Eleventh International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_1_30_1","unstructured":"Chang Liu Xiwei Wu Yuan Feng Qinxiang Cao and Junchi Yan. 2025. Towards general loop invariant generation: a benchmark of programs with memory manipulation. Article 4101 26 pages. isbn:9798331314385"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115691"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Saswat Padhi Rahul Sharma and Todd Millstein. 2016. Data-driven precondition inference with learned features. 42\u201356. isbn:9781450342612 https:\/\/doi.org\/10.1145\/2908080.2908099 10.1145\/2908080.2908099","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549166"},{"key":"e_1_2_1_36_1","volume-title":"International Conference on Learning Representations (ICLR).","author":"Ryan Gabriel","year":"2020","unstructured":"Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_2_1_41_1","unstructured":"Xujie Si Hanjun Dai Mukund Raghothaman Mayur Naik and Le Song. 2018. Learning loop invariants for program verification. 7762\u20137773."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Hari Govind Vediramana Krishnan YuTing Chen Sharon Shoham and Arie Gurfinkel. 2020. Global Guidance for Local Generalization in Model Checking. 101\u2013125. isbn:978-3-030-53290-1 https:\/\/doi.org\/10.1007\/978-3-030-53291-8_7 10.1007\/978-3-030-53291-8_7","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695014"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409752"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598047"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"He Zhu Stephen Magill and Suresh Jagannathan. 2018. A data-driven CHC solver. 707\u2013721. isbn:9781450356985 https:\/\/doi.org\/10.1145\/3192366.3192416 10.1145\/3192366.3192416","DOI":"10.1145\/3192366.3192416"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784766"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728920","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:52:03Z","timestamp":1752684723000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728920"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":49,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728920"],"URL":"https:\/\/doi.org\/10.1145\/3728920","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}