{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:06Z","timestamp":1783545306222,"version":"3.55.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT\/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebraic data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_6","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:22Z","timestamp":1779024022000},"page":"111-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Can LLM Aid in\u00a0Solving Constraints with\u00a0Inductive Definitions?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0710-223X","authenticated-orcid":false,"given":"Weizhi","family":"Feng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0369-021X","authenticated-orcid":false,"given":"Shidong","family":"Shen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6725-8167","authenticated-orcid":false,"given":"Jiaxiang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5993-1665","authenticated-orcid":false,"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0581-2679","authenticated-orcid":false,"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0899-628X","authenticated-orcid":false,"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"6_CR1","unstructured":"Alhessi, Y., et al.: Lemmanaid: neuro-symbolic lemma conjecturing (2025). https:\/\/arxiv.org\/abs\/2504.04942"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I, vol. 13243, pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"6_CR3","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Cham (2013)"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, SCALA@ECOOP, pp. 1:1\u20131:10. ACM (2013). https:\/\/doi.org\/10.1145\/2489837.2489838","DOI":"10.1145\/2489837.2489838"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Cao, W., et al.: Clause2inv: a generate-combine-check framework for loop invariant inference. Proc. ACM Softw. Eng. 2(ISSTA), 1009\u20131030 (2025). https:\/\/doi.org\/10.1145\/3728920","DOI":"10.1145\/3728920"},{"key":"6_CR6","unstructured":"Chuharski, J., Collins, E.R., Meringolo, M.: Mining math conjectures from LLMs: a pruning approach (2024). https:\/\/arxiv.org\/abs\/2412.16177"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-66167-4_10","volume-title":"Frontiers of Combining Systems","author":"S Cruanes","year":"2017","unstructured":"Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172\u2013188. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_10"},{"issue":"3\u20134","key":"6_CR9","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1017\/S1471068418000157","volume":"18","author":"E De Angelis","year":"2018","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Solving horn clauses on inductive data types without induction. Theory Pract. Log. Program. 18(3\u20134), 452\u2013469 (2018). https:\/\/doi.org\/10.1017\/S1471068418000157","journal-title":"Theory Pract. Log. Program."},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-030-51074-9_6","volume-title":"Automated Reasoning","author":"E De Angelis","year":"2020","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Removing algebraic data types from constrained horn clauses using difference predicates. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 83\u2013102. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_6"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83\u201398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30142-4_7"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"issue":"2","key":"6_CR13","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/S10817-019-09519-X","volume":"64","author":"M Echenim","year":"2020","unstructured":"Echenim, M., Peltier, N.: Combining induction and saturation-based theorem proving. J. Autom. Reason. 64(2), 253\u2013294 (2020). https:\/\/doi.org\/10.1007\/S10817-019-09519-X","journal-title":"J. Autom. Reason."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Gauthier, T., Urban, J.: Learning conjecturing from scratch (2025). https:\/\/arxiv.org\/abs\/2503.01389","DOI":"10.1007\/978-3-031-99984-0_23"},{"key":"6_CR15","unstructured":"Guo, D., et\u00a0al.: Deepseek-coder: when the large language model meets programming\u2013the rise of code intelligence. arXiv preprint arXiv:2401.14196 (2024)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-030-53518-6_8","volume-title":"Intelligent Computer Mathematics","author":"M Hajd\u00fa","year":"2020","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 123\u2013137. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_8"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), pp. 1\u201310. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_34","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_34"},{"key":"6_CR18","unstructured":"Hajd\u00fa, M., Kov\u00e1cs, L., Rawson, M., Voronkov, A.: The vampire approach to induction (short paper). In: Proceedings of the Workshop on Practical Aspects of Automated Reasoning (IJCAR), vol.\u00a03201 (2022)"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kuncak, V.: System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA), 166:1\u2013166:30 (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-030-79876-5_21","volume-title":"Automated Deduction \u2013 CADE 28","author":"P Hozzov\u00e1","year":"2021","unstructured":"Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Integer induction in saturation. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 361\u2013377. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_21"},{"issue":"1\u20132","key":"6_CR21","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A Ireland","year":"1996","unstructured":"Ireland, A.: Productive use of failure in inductive proof. J. Autom. Reason. 16(1\u20132), 79\u2013111 (1996). https:\/\/doi.org\/10.1007\/BF00244460","journal-title":"J. Autom. Reason."},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"K., H.G.V., Shoham, S., Gurfinkel, A.: Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498722","DOI":"10.1145\/3498722"},{"key":"6_CR23","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M Kaufmann","year":"2013","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies, vol. 4. Springer, Cham (2013)"},{"issue":"3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Kurashige, C., et al.: CCLemma: E-graph guided lemma discovery for inductive equational proofs. Proc. ACM Program. Lang. 8(ICFP), 818\u2013844 (2024)","DOI":"10.1145\/3674653"},{"issue":"OOPSLA1","key":"6_CR27","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1145\/3586037","volume":"7","author":"A Lattuada","year":"2023","unstructured":"Lattuada, A.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023). https:\/\/doi.org\/10.1145\/3586037","journal-title":"Proc. ACM Program. Lang."},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Li, L., Sleem, L., Gentile, N., Nichil, G., State, R.: Exploring the impact of temperature on large language models: hot or cold? CoRR abs\/2506.07295 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2506.07295","DOI":"10.48550\/ARXIV.2506.07295"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Lv, K., Dong, Y., Han, R., Jia, F., Ma, F., Zhang, J.: LLM-guided quantified SMT solving over uninterpreted functions (2026). https:\/\/arxiv.org\/abs\/2601.04675","DOI":"10.1609\/aaai.v40i17.38445"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: automated generation of formal program specifications via large language models. In: Proceedings of the IEEE\/ACM 47th International Conference on Software Engineering (ICSE), pp. 16\u201328 (2025). https:\/\/doi.org\/10.1109\/ICSE55347.2025.00129","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer, Cham (1994)","DOI":"10.1007\/BFb0030541"},{"key":"6_CR35","unstructured":"Peled, R., Kroening, D., Tautschnig, M., Vizel, Y.: Large lemma miners: can LLMs do induction proofs for hardware? (2025). https:\/\/arxiv.org\/abs\/2511.02521"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Pirzada, M.A.A., Reger, G., Bhayat, A., Cordeiro, L.C.: LLM-generated invariants for bounded model checking without loop unrolling. In: Filkov, V., Ray, B., Zhou, M. (eds.) Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, pp. 1395\u20131407. ACM (2024). https:\/\/doi.org\/10.1145\/3691620.3695512","DOI":"10.1145\/3691620.3695512"},{"key":"6_CR37","unstructured":"Reger, G., Suda, M., Voronkov, A.: Instantiation and pretending to be an SMT solver with vampire. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22 - 23, 2017. CEUR Workshop Proceedings, vol.\u00a01889, pp. 63\u201375. CEUR-WS.org (2017). https:\/\/ceur-ws.org\/Vol-1889\/paper6.pdf"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-030-29436-6_28","volume-title":"Automated Deduction \u2013 CADE 27","author":"G Reger","year":"2019","unstructured":"Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 477\u2013494. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_28"},{"key":"6_CR39","unstructured":"Ren, Z.Z., et al.: Deepseek-prover-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition (2025). https:\/\/arxiv.org\/abs\/2504.21801"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Silva, \u00c1., Mendes, A., Ferreira, J.F.: Leveraging large language models to boost Dafny\u2019s developers productivity. In: Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 138\u2013142 (2024)","DOI":"10.1145\/3644033.3644374"},{"key":"6_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-81688-9_6","volume-title":"Computer Aided Verification","author":"E Singher","year":"2021","unstructured":"Singher, E., Itzhaky, S.: Theory exploration powered by deductive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 125\u2013148. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6"},{"key":"6_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Sonnex","year":"2012","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407\u2013421. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28"},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"Sun, Y., Ji, R., Fang, J., Jiang, X., Chen, M., Xiong, Y.: Proving functional program equivalence via directed lemma synthesis. In: Proceedings of the 26th International Symposium on Formal Methods (FM), Part I, vol. 14933, pp. 538\u2013557. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_28","DOI":"10.1007\/978-3-031-71162-6_28"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Sun, Z., Du, X., Song, F., Wang, S., Li, L.: When neural code completion models size up the situation: attaining cheaper and faster completion through dynamic model inference. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering (ICSE), pp. 1\u201312 (2024)","DOI":"10.1145\/3597503.3639120"},{"issue":"1","key":"6_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3688831","volume":"34","author":"Z Sun","year":"2025","unstructured":"Sun, Z., et al.: Don\u2019t complete it! preventing unhelpful code completion for productive and sustainable neural code completion systems. ACM Trans. Softw. Eng. Methodol. 34(1), 1\u201322 (2025)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR47","unstructured":"Varambally, S., Voice, T., Sun, Y., Chen, Z., Yu, R., Ye, K.: Hilbert: recursively building formal proofs with informal reasoning (2025). https:\/\/arxiv.org\/abs\/2509.22819"},{"key":"6_CR48","unstructured":"Wang, H., et al.: Kimina-prover preview: towards large formal reasoning models with reinforcement learning (2025). https:\/\/arxiv.org\/abs\/2504.11354"},{"key":"6_CR49","doi-asserted-by":"publisher","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Proceedings of the International Conference on Computer Aided Verification (CAV), pp. 302\u2013328. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"6_CR50","doi-asserted-by":"publisher","unstructured":"Wu, G., Cao, W., Yao, Y., Wei, H., Chen, T., Ma, X.: LLM meets bounded model checking: Neuro-symbolic loop invariant inference. In: Filkov, V., Ray, B., Zhou, M. (eds.) Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024, pp. 406\u2013417. ACM (2024). https:\/\/doi.org\/10.1145\/3691620.3695014","DOI":"10.1145\/3691620.3695014"},{"issue":"OOPSLA2","key":"6_CR51","doi-asserted-by":"publisher","first-page":"3454","DOI":"10.1145\/3763174","volume":"9","author":"C Yang","year":"2025","unstructured":"Yang, C., et al.: Autoverus: automated proof generation for rust code. Proc. ACM Program. Lang. 9(OOPSLA2), 3454\u20133482 (2025). https:\/\/doi.org\/10.1145\/3763174","journal-title":"Proc. ACM Program. Lang."},{"issue":"9","key":"6_CR52","doi-asserted-by":"publisher","first-page":"2437","DOI":"10.1109\/TSE.2024.3440503","volume":"50","author":"G Yang","year":"2024","unstructured":"Yang, G., Zhou, Y., Chen, X., Zhang, X., Zhuo, T.Y., Chen, T.: Chain-of-thought in neural code generation: From and for lightweight language models. IEEE Trans. Softw. Eng. 50(9), 2437\u20132457 (2024)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-030-30048-7_35","volume-title":"Principles and Practice of Constraint Programming","author":"W Yang","year":"2019","unstructured":"Yang, W., Fedyukovich, G., Gupta, A.: Lemma synthesis for automating induction over algebraic data types. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 600\u2013617. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_35"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:28Z","timestamp":1783542568000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}