ClassInvGen: Class Invariant Synthesis Using Large Language Models. Sun, C., Agashe, V., Chakraborty, S., Taneja, J., Barrett, C., Dill, D., Qiu, X., & Lahiri, S. K. In Giacobbe, M. & Lukina, A., editors, AI Verification, pages 64–96, Cham, 2026. Springer Nature Switzerland. doi abstract bibtex Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants.
@inproceedings{sun_classinvgen_2026,
address = {Cham},
title = {{ClassInvGen}: {Class} {Invariant} {Synthesis} {Using} {Large} {Language} {Models}},
isbn = {978-3-031-99991-8},
shorttitle = {{ClassInvGen}},
doi = {10.1007/978-3-031-99991-8_4},
abstract = {Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants.},
language = {en},
booktitle = {{AI} {Verification}},
publisher = {Springer Nature Switzerland},
author = {Sun, Chuyue and Agashe, Viraj and Chakraborty, Saikat and Taneja, Jubi and Barrett, Clark and Dill, David and Qiu, Xiaokang and Lahiri, Shuvendu K.},
editor = {Giacobbe, Mirco and Lukina, Anna},
year = {2026},
keywords = {Class Invariants, Formal Verification, Large Language Models, Program Synthesis},
pages = {64--96},
}
Downloads: 0
{"_id":"XqZPor73r73WLsdxk","bibbaseid":"sun-agashe-chakraborty-taneja-barrett-dill-qiu-lahiri-classinvgenclassinvariantsynthesisusinglargelanguagemodels-2026","author_short":["Sun, C.","Agashe, V.","Chakraborty, S.","Taneja, J.","Barrett, C.","Dill, D.","Qiu, X.","Lahiri, S. K."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Cham","title":"ClassInvGen: Class Invariant Synthesis Using Large Language Models","isbn":"978-3-031-99991-8","shorttitle":"ClassInvGen","doi":"10.1007/978-3-031-99991-8_4","abstract":"Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants.","language":"en","booktitle":"AI Verification","publisher":"Springer Nature Switzerland","author":[{"propositions":[],"lastnames":["Sun"],"firstnames":["Chuyue"],"suffixes":[]},{"propositions":[],"lastnames":["Agashe"],"firstnames":["Viraj"],"suffixes":[]},{"propositions":[],"lastnames":["Chakraborty"],"firstnames":["Saikat"],"suffixes":[]},{"propositions":[],"lastnames":["Taneja"],"firstnames":["Jubi"],"suffixes":[]},{"propositions":[],"lastnames":["Barrett"],"firstnames":["Clark"],"suffixes":[]},{"propositions":[],"lastnames":["Dill"],"firstnames":["David"],"suffixes":[]},{"propositions":[],"lastnames":["Qiu"],"firstnames":["Xiaokang"],"suffixes":[]},{"propositions":[],"lastnames":["Lahiri"],"firstnames":["Shuvendu","K."],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Giacobbe"],"firstnames":["Mirco"],"suffixes":[]},{"propositions":[],"lastnames":["Lukina"],"firstnames":["Anna"],"suffixes":[]}],"year":"2026","keywords":"Class Invariants, Formal Verification, Large Language Models, Program Synthesis","pages":"64–96","bibtex":"@inproceedings{sun_classinvgen_2026,\n\taddress = {Cham},\n\ttitle = {{ClassInvGen}: {Class} {Invariant} {Synthesis} {Using} {Large} {Language} {Models}},\n\tisbn = {978-3-031-99991-8},\n\tshorttitle = {{ClassInvGen}},\n\tdoi = {10.1007/978-3-031-99991-8_4},\n\tabstract = {Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants.},\n\tlanguage = {en},\n\tbooktitle = {{AI} {Verification}},\n\tpublisher = {Springer Nature Switzerland},\n\tauthor = {Sun, Chuyue and Agashe, Viraj and Chakraborty, Saikat and Taneja, Jubi and Barrett, Clark and Dill, David and Qiu, Xiaokang and Lahiri, Shuvendu K.},\n\teditor = {Giacobbe, Mirco and Lukina, Anna},\n\tyear = {2026},\n\tkeywords = {Class Invariants, Formal Verification, Large Language Models, Program Synthesis},\n\tpages = {64--96},\n}\n\n\n\n","author_short":["Sun, C.","Agashe, V.","Chakraborty, S.","Taneja, J.","Barrett, C.","Dill, D.","Qiu, X.","Lahiri, S. K."],"editor_short":["Giacobbe, M.","Lukina, A."],"key":"sun_classinvgen_2026","id":"sun_classinvgen_2026","bibbaseid":"sun-agashe-chakraborty-taneja-barrett-dill-qiu-lahiri-classinvgenclassinvariantsynthesisusinglargelanguagemodels-2026","role":"author","urls":{},"keyword":["Class Invariants","Formal Verification","Large Language Models","Program Synthesis"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/alukina","dataSources":["Cfgnp5s4HQSBd8tAf"],"keywords":["class invariants","formal verification","large language models","program synthesis"],"search_terms":["classinvgen","class","invariant","synthesis","using","large","language","models","sun","agashe","chakraborty","taneja","barrett","dill","qiu","lahiri"],"title":"ClassInvGen: Class Invariant Synthesis Using Large Language Models","year":2026}