{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:36Z","timestamp":1776305256490,"version":"3.50.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999901","type":"print"},{"value":"9783031999918","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:00:00Z","timestamp":1761609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-99991-8_4","type":"book-chapter","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:36:01Z","timestamp":1761543361000},"page":"64-96","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["ClassInvGen: Class Invariant Synthesis Using Large Language Models"],"prefix":"10.1007","author":[{"given":"Chuyue","family":"Sun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viraj","family":"Agashe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saikat","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jubi","family":"Taneja","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,28]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201902, pp. 4\u201316. Association for Computing Machinery, New York (2002). https:\/\/doi.org\/10.1145\/503272.503275","DOI":"10.1145\/503272.503275"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-031-57259-3_7","volume-title":"Fundamental Approaches to Software Engineering","author":"JH Boockmann","year":"2024","unstructured":"Boockmann, J.H., L\u00fcttgen, G.: Comprehending object state via dynamic class invariant learning. In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering, pp. 143\u2013164. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57259-3_7"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Brunsfeld, M., et al.: Kolja: tree-sitter\/tree-sitter: v0.24.4 (2024). https:\/\/doi.org\/10.5281\/zenodo.14061403","DOI":"10.5281\/zenodo.14061403"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of jml tools and applications. Int. J. Softw. Tools Technol. Transfer 7, 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI\u201908, pp. 209\u2013224. USENIX Association (2008)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Csallner, C., Tillmann, N., Smaragdakis, Y.: Dysy: dynamic symbolic execution for invariant inference. In: Proceedings of the 30th International Conference on Software Engineering, ICSE \u201908, pp. 281\u2013290. Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1368088.1368127","DOI":"10.1145\/1368088.1368127"},{"key":"4_CR8","unstructured":"Dimitrios, A.: Algorithms and data structures (2023). https:\/\/github.com\/djeada\/Algorithms-And-Data-Structures\/tree\/master\/src\/collections_and_containers\/cpp"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Endres, M., Fakhoury, S., Chakraborty, S., Lahiri, S.K.: Can large language models transform natural language intent into formal method postconditions? Proc. ACM Softw. Eng. 1(FSE) (2024). https:\/\/doi.org\/10.1145\/3660791","DOI":"10.1145\/3660791"},{"issue":"1\u20133","key":"4_CR10","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15769-1_2","volume-title":"Static Analysis","author":"M F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M.: Static verification for code contracts. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 2\u20135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_2"},{"key":"4_CR12","unstructured":"Gao, Y., et al.: Retrieval-augmented generation for large language models: a survey. arXiv preprint arXiv:2312.10997 (2023)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201916, pp. 499\u2013512. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2837614.2837664","DOI":"10.1145\/2837614.2837664"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Greiner, S., B\u00fchlmann, N., Ohrndorf, M., Tsigkanos, C., Nierstrasz, O., Kehrer, T.: Automated generation of code contracts: Generative ai to the rescue? In: Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pp. 1\u201314 (2024)","DOI":"10.1145\/3689484.3690738"},{"key":"4_CR16","unstructured":"Hellendoorn, V.J., Devanbu, P.T., Polozov, A., Marron, M.: Are my invariants valid? a learning approach. arXiv preprint (2019). https:\/\/www.microsoft.com\/en-us\/research\/publication\/are-my-invariants-valid-a-learning-approach\/"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"4_CR18","unstructured":"Kamath, A., et al.: Finding inductive loop invariants using large language models (2023). https:\/\/arxiv.org\/abs\/2311.07948"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"4_CR20","unstructured":"Lahiri, S.: Evaluating llm-driven user-intent formalization for verification-aware languages. In: Formal Methods in Computer-Aided Design (FMCAD\u201924) (2024). https:\/\/www.microsoft.com\/en-us\/research\/publication\/evaluating-llm-driven-user-intent-formalization-for-verification-aware-languages\/"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 493\u2013508. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_37"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: Llvm: a compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization, 2004, CGO 2004, pp. 75\u201386 (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"OOPSLA1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1145\/3586037","volume":"7","author":"A Lattuada","year":"2023","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Le, T.C., Zheng, G., Nguyen, T.: Sling: using dynamic analysis to infer program invariants in separation logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 788\u2013801. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314634","DOI":"10.1145\/3314221.3314634"},{"key":"4_CR25","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":"4_CR26","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Inala, J.P., Lahiri, S.K., Sen, S.: Codamosa: escaping coverage plateaus in test generation with pre-trained large language models. In: Proceedings of the 45th International Conference on Software Engineering, ICSE \u201923, pp. 919\u2013931. IEEE Press (2023). https:\/\/doi.org\/10.1109\/ICSE48619.2023.00085","DOI":"10.1109\/ICSE48619.2023.00085"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1162\/tacl_a_00638","volume":"12","author":"NF Liu","year":"2024","unstructured":"Liu, N.F., et al.: Lost in the middle: how language models use long contexts. Trans. Assoc. Comput. Linguist. 12, 157\u2013173 (2024)","journal-title":"Trans. Assoc. Comput. Linguist."},{"key":"4_CR28","unstructured":"Lohmann, N., et al.: mutate_cpp - mutation testing tool for c++ (2017). https:\/\/github.com\/nlohmann\/mutate_cpp"},{"key":"4_CR29","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. CoRR arxiv:2401.08807 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.08807","DOI":"10.48550\/ARXIV.2401.08807"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_2"},{"key":"4_CR31","unstructured":"Meyer, B.: The eiffel programming language (1992). http:\/\/www.eiffel.com"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Molina, F., d\u2019Amorim, M., Aguirre, N.: Fuzzing class specifications. In: Proceedings of the 44th International Conference on Software Engineering, ICSE \u201922, pp. 1008\u20131020. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3510003.3510120","DOI":"10.1145\/3510003.3510120"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient smt solver. In: 2008 Tools and Algorithms for Construction and Analysis of Systems, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/z3-an-efficient-smt-solver\/","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR34","unstructured":"Newcomb, J.L., Bodik, R.: Using human-in-the-loop synthesis to author functional reactive programs (2019). https:\/\/arxiv.org\/abs\/1909.11206"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 683\u2013693 (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227149","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13\u201317 June 2016, pp. 42\u201356 (2016). https:\/\/doi.org\/10.1145\/2908080.2908099","DOI":"10.1145\/2908080.2908099"},{"key":"4_CR37","unstructured":"Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., Scarlett, J. (eds.) Proceedings of the 40th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a0202, pp. 27496\u201327520. PMLR (2023). https:\/\/proceedings.mlr.press\/v202\/pei23a.html"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Ciupa, I., Meyer, B.: A comparative study of programmer-written and automatically inferred contracts. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 93\u2013104 (2009)","DOI":"10.1145\/1572272.1572284"},{"key":"4_CR39","unstructured":"Sch\u00e4fer, M., Nadi, S., Eghbali, A., Tip, F.: An empirical evaluation of using large language models for automated unit test generation (2023). https:\/\/arxiv.org\/abs\/2302.06527"},{"issue":"9","key":"4_CR40","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/2034574.2034811","volume":"46","author":"N Swamy","year":"2011","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. ACM SIGPLAN Not. 46(9), 266\u2013278 (2011)","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR41","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-031-65630-9_16","volume-title":"Computer Aided Verification","author":"C Wen","year":"2024","unstructured":"Wen, C., et al.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 302\u2013328. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_16"},{"key":"4_CR42","unstructured":"Wikipedia contributors: Avl tree\u2014Wikipedia, the free encyclopedia (2024). https:\/\/en.wikipedia.org\/w\/index.php?title=AVL_tree&oldid=1255561501. Accessed 15 Nov 2024"},{"key":"4_CR43","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: Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering, ASE \u201924, pp. 406\u2013417. Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3691620.3695014","DOI":"10.1145\/3691620.3695014"},{"issue":"OOPSLA2","key":"4_CR44","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1145\/3689736","volume":"8","author":"C Yang","year":"2024","unstructured":"Yang, C., et al.: Whitefox: white-box compiler fuzzing empowered by large language models. Proc. ACM Program. Lang. 8(OOPSLA2), 709\u2013735 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR45","unstructured":"z3Prover: z3prover util classes (2024). https:\/\/github.com\/Z3Prover\/z3\/tree\/master\/src\/util"}],"container-title":["Lecture Notes in Computer Science","AI Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99991-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T05:36:10Z","timestamp":1761543370000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99991-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,28]]},"ISBN":["9783031999901","9783031999918"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99991-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,28]]},"assertion":[{"value":"28 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAIV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on AI Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"saiv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.aiverification.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}