ClassInvGen: Class Invariant Synthesis Using Large Language Models

doi:10.1007/978-3-031-99991-8_4

ClassInvGen: Class Invariant Synthesis Using Large Language Models

2026-01-01

0

PRE

AI

DOI：10.1007/978-3-031-99991-8_4

Original

Original request for help

Save

Abstract

En 中文

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. In this work, we describe ClassInvGen, a method for co-generating executable class invariants and test inputs to produce high-quality class invariants for a mainstream language such as C++, leveraging LLMs' ability to synthesize pure functions. We demonstrate that ClassInvGen outperforms a pure LLM-based technique for generating specifications (from code) as well as prior data-driven invariant inference techniques such as Daikon. We contribute a benchmark of standard C++ data structures along with a harness that can help measure both the correctness and completeness of generated specifications using tests and mutants. We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++ codebase.

Keywords:

Program Synthesis

Large Language Models

Class Invariants

Formal Verification

ClassInvGen: Class Invariant Synthesis Using Large Language Models

Abstract

Journal

Organization