arXiv:2605.27051v1 [cs.SE] 26 May 2026
C ON V ER: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification Muhammad A. A. Pirzada*
Weiqi Wang*
Yiannis Charalambous*
The University of Manchester Manchester, UK 0009-0005-2440-7547
The University of Manchester Manchester, UK 0009-0005-8247-5994
The University of Manchester Manchester, UK 0009-0000-5755-5099
Konstantin Korovin
Lucas C. Cordeiro
The University of Manchester Manchester, UK 0000-0002-0740-621X
The University of Manchester Manchester, UK 0000-0002-6235-4272
Abstract—Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present C ON V ER, a top-down compositional verification tool. Given a C program with a top-level assertion, C ON V ER decomposes verification topdown: it uses a large language model (LLM) to synthesise function contracts from the system property, then alternates system-level and function-level checks in a CEGAR-CEGIS loop, refining contracts whenever a check fails via SMART ICE learning. We evaluate C ON V ER on four benchmark suites of increasing difficulty and against other state-of-the-art (SOTA) tools. On the Frama-C benchmark of 45 simple C programs, C ON V ER achieves 82–96% verification success across three LLM backends, with 93–95% of converged programs requiring only a single CEGAR-CEGIS iteration. On the X.509 parser benchmark (6 programs) and LF2C-Simple suite (17 programs), C ON V ER achieves 33–50% and 82–88% success respectively. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55–64% success. In addition, we present ESBMC-LF a preprocessor tool that converts LF models to C while preserving the properties of the LF files, enabling C ON V ER to verify them. We transpile the LF Verifier Benchmarks using ESBMC-LF to C; we denote those LF-Hard. We show that C ON V ER successfully verifies 67% of LF-Hard benchmarks overall. Index Terms—Formal Verification, Compositional Verification, Contract Synthesis, Large Language Models, CEGAR, CEGIS
I. I NTRODUCTION Verifying the correctness of large C programs is one of the central challenges in software engineering and formal verification. BMC tools such as the Efficient SMT-based ContextBounded Model Checker (ESBMC) [1] and C Bounded Model Checker (CBMC) [2] are highly effective on self-contained functions and small-scale models, but their complexity grows rapidly with program size: every function call adds to the state space that the underlying SMT solver must explore, and every loop requires unrolling up to a max bound. These contribute to the well-known state explosion problem in software model checking [3]. The standard method of writing * These authors contributed equally to this work.
function contracts by hand is expert-intensive and poorly adopted in practice; even well-resourced projects such as AWS’s s2n-tls [2] require dedicated annotation effort from verification engineers. The result is that formal verification remains largely inaccessible for programs exceeding a few hundred lines. C ON V ER addresses this gap by combining two complementary ideas. First, it adopts a top-down property decomposition strategy: rather than starting from individual function specifications and building upward, it begins with an abstract systemlevel assertion in main() and derives function contracts sufficient to prove that property. This top-down view minimises the specification burden as contracts need to only capture what the system property requires, not every semantic property of the underlying function. Second, C ON V ER automates contract synthesis and refinement with Large Language Models (LLMs). An LLM proposes initial contracts; a software verification tool then checks them at the system level (by replacing calls with contract stubs) and at the function level (by verifying each implementation against its contract). Failures are then fed back to the LLM as structured counterexamples through a Counterexample Guided Abstraction Refinement (CEGAR) [4] loop augmented with SMART Implication Counterexamples (ICE) learning [5], which classifies each counterexample into positive, negative, and implication examples to guide targeted refinement. C ON V ER uses ESBMC for software verification. a) Contributions.: The main contributions of this paper are: 1) Top-down contract derivation. A methodology that derives function contracts directly from a system-level assertion, minimising manual specification effort. 2) CEGAR with SMART ICE learning. An iterative refinement loop that classifies ESBMC counterexamples into positive, negative, and implication examples to guide targeted LLM re-synthesis. 3) Loop invariant synthesis. An on-demand inductive invariant generation step for functions where bounded checking is insufficient, integrated seamlessly into the
simplifies the SMT equation and focuses on encoding only the model to be verified. Making the verification process simpler. Used as a Preprocessor tool to enable C ON V ER to verify LF benchmarks. We investigate three research questions throughout the paper. RQ1 How effectively does C ON V ER verify programs across diverse benchmarks, and how does performance compare across three LLM backends?
RQ2 Under what conditions does SMART ICE learning improve convergence, and how does the quality of counterexample feedback interact with LLM capability?
RQ3 How does C ON V ER scale to larger, structurally complex programs?
Fig. 1. The C ON V ER verification pipeline. The LLM derives function contracts top-down from the system property; the CEGAR loop alternates system-level and function-level ESBMC checks, refining contracts via ICE learning until both levels pass.
Counterexample Guided Inductive Synthesis (CEGIS) loop. 4) End-to-end evaluation. An empirical study across four benchmarks: the Frama-C benchmark (45 programs, 82– 96% success), LF2C-Simple (17 programs, 82–88%), X.509 parser programs (6 programs, 33–50%), and VerifyThis recursive/loop-intensive programs (11 programs, 55–64%), covering diverse program structures and verification challenges. 5) ESBMC-LF. A prototype preprocessor transpilation tool used to convert Lingua Franca (LF) benchmarks to Cbased models, for verification with tools that work on the C programming language. Created for LF-Hard, comprising 24 LF Benchmarks that are converted into a monolithic C version. With the operational models of the LF Reactor replacing the implementation, this therefore
The remainder of the paper is organised as follows. Section II covers background and Section III covers similar research to C ON V ER. Section IV presents the C ON V ER methodology. Section V presents the benchmarks that C ON V ER will be tested on, along with the ESBMC-LF preprocessor. Section VI reports experimental results. Section VII discusses findings and threats to validity. Section VIII discusses conclusions from the research. II. BACKGROUND a) Bounded Model Checking (BMC): [6], [7] verifies program correctness by unrolling loops up to a bound k and encoding the resulting acyclic program as an SMT formula: a satisfying assignment corresponds to a counterexample, while unsatisfiability proves correctness up to bound k. ESBMC [1], [8]–[10] is a mature BMC tool that supports C/C++ with rich arithmetic and pointer reasoning. The fundamental limitation of BMC is state space explosion: for large programs with many functions and deep call stacks, the SMT instance grows rapidly and solver time increases rapidly. Function contracts are the standard mitigation technique. Once a function is verified against its contract, the contract replaces the implementation in all calling contexts, preventing the solver from re-exploring the function’s internals. b) Large Language Models.: Recent work demonstrates that LLMs can reason effectively about code structure and semantics [11]–[16]. LLMs have been applied to test generation, bug finding, and program synthesis, and more recently
to formal specification tasks such as precondition and postcondition derivation [17], [18] C ON V ER uses LLMs solely for contract and invariant synthesis for proposing candidate formal annotations, but delegates verification decisions to ESBMC, making the verification sound. This separation ensures that soundness depends only on the model checker, not on the LLM’s output. III. R ELATED W ORK a) PolyVer: Many real-world software systems are polyglot: their components are implemented in different programming languages, yet traditional verifiers target a single language, making whole-system verification challenging. PolyVer [17] addresses this by combining abstraction, compositional reasoning, and contract synthesis to verify polyglot systems. The system is modelled as a transition system whose components may be coded in different languages (e.g., C or Rust); PolyVer connects a top-level model checker (UCLID5 [19]) with language-specific back-ends (CBMC for C, Kani for Rust) via automatically synthesised precondition/postcondition contracts at each language boundary. C ON V ER is thematically related: both tools decompose cross-component verification through contracts, but C ON V ER operates within a single language (C) and automates contract synthesis via LLMs rather than requiring manual annotation. Additionally, C ON V ER uses ESBMC-LF to create C-based models of LF benchmarks to automatically verify them. b) ACSE: Array-Carrying Symbolic Execution (ACSE) [20] automates function contract generation for array-manipulating C programs via a symbolic execution framework that carries invariants and contiguous array segments along execution paths. ACSE propagates loop invariants from external generators, handles disjunctive loop exits, and merges or splits array segments to synthesise precise ACSL pre/postconditions and assigns clauses, which are then discharged by Frama-C’s WP plugin. C ON V ER is complementary: both tools target automated contract synthesis, but ACSE derives contracts analytically in a single symbolic pass and crucially supports quantified array invariants (e.g., ∀i. a[i] ≥ 0) that ESBMC’s contract mechanism cannot express. C ON V ER instead synthesises contracts via LLMs and iteratively refines them against formal counterexamples in a CEGAR/CEGIS loop, handling cases where symbolic invariant inference is imprecise or the program is too large for exhaustive symbolic exploration. IV. M ETHODOLOGY This Section will describe the functionality behind C ON V ER and provide an overview of the function contract and loop invariant integration. Algorithm 1 covers how C ON V ER works. C ON V ER verifies a C program compositionally by decomposing its top-level system property into per-function contracts that are independently checkable by a formal verification tool. This abstraction of the state space enables verification of programs larger than would be possible with traditional formal
verifiers due to state explosion. The verification happens at the following levels: • At the system level (Step 3), every function call is replaced by a contract: ESBMC checks whether the system assertion holds assuming each function satisfies its postcondition, without exploring any function internals. • At the function level (Step 4), each implementation is checked against its own contract in isolation: ESBMC assumes the precondition holds and asserts the postcondition after execution, verifying the actual source code of that function. Algorithm 1 Overview of C ON V ER Require: Program P , complexity threshold τ , max iterations K Ensure: Verified ⊤ or Falsified ⊥ 1: Step 1 — Derive Sets 2: φ ← E XTRACT P ROPERTY(P ) 3: F ← E XTRACT F UNCTIONS(P ) \ { MAIN} 4: FL = {f ∈ F | σ(f ) < τ } ▷ Low complexity functions FH = {f ∈ F | σ(f ) ≥ τ } ▷ High complexity functions 5: Step 2 — Preprocessing ▷ Run if Pre-Abstraction is enabled 6: CL ← S YNTHESIZE (FL , φ) ▷ Simple; can verify directly 7: CH ← OVERAPPROXIMATE(FH , φ) ▷ State explosion; too complex to verify directly 8: C ← CL ∪ CH 9: Step 3 — System-Level Verification 10: VS ← V ERIFY S YSTEM (P, C) 11: Step 4 — Function-Level Verification 12: Vf ← V ERIFY F UNCTION (P, C, f ) ▷ For all f ∈ F 13: if PASS(VS ) ∧ ∀f ∈ F : PASS(Vf ) then 14: return ⊤ ▷ Contracts correct without refinement 15: end if 16: Step 5 — Contract Replacement and System Verification 17: C ← {Cf ∈ C | PASS(Vf )} ▷ Drop contracts that failed function-level verification 18: VS ← V ERIFY S YSTEM (P, C) ▷ Verify using surviving contracts 19: Step 6 — CEGAR Refinement 20: ⟨C, VS , VF ⟩ ← CEGAR(C, VS , VF , K) ▷ See Alg. 2 21: if PASS(VS ) ∧ ∀v ∈ VF : PASS(v) then 22: return ⊤ 23: end if 24: Step 7 — CEGIS Escalation 25: ⟨C, VS , VF ⟩ ← CEGIS(C, VS , VF , K) ▷ See Alg. 3 26: if PASS(VS ) ∧ ∀v ∈ VF : PASS(v) then 27: return ⊤ 28: end if 29: return ⊥ ConVer uses a two-stage refinement strategy. Both stages verify contracts at the system level (proving the property holds assuming contracts — Step 3) and the function level (proving each implementation satisfies its contract — Step
4). The CEGAR loop first attempts to refine contracts using LLM-guided counterexample analysis (Step 5). If CEGAR stagnates, a variant of Delta Debugging [21], [22] is used as a stagnation breaker by incrementally removing post-condition clauses from stagnating functions, reverifies said function until the verification passes, then pipeline escalates to CEGIS (Step 7). CEGIS performs constraint-based synthesis against accumulated positive and negative examples. LLMs are integrated into both loops to facilitate contract generation. A. ESBMC Function Contract and Loop Invariant Checker ESBMC [1] supports modular verification through two complementary mechanisms: function contracts and loop invariants. Function contracts support deductive reasoning —deriving postconditions from preconditions without reexamining the function body—while loop invariants support inductive reasoning, establishing correctness for unbounded1 loops through a fixed base case and preservation argument.2 Together, they form the verification backbone of C ON V ER,3 enabling large-scale verification tasks to be decomposed into 4 independently checkable units. a) Function Contracts.: A function contract for a func-5 tion f is a triple (P, Q, S), where P : State → B is the precondition, Q : State × State → B is the postcondition relating pre- and post-states, and S ⊆ Vars is the assigns set of locations f is permitted to modify. In ESBMC these are expressed via __ESBMC_requires, __ESBMC_ensures, and __ESBMC_assigns. A simple example is shown below: 1 2 3 4
5 6
int increment(int x) { __ESBMC_requires(x > 0); __ESBMC_assigns(x); __ESBMC_ensures(__ESBMC_return_value > x); return x + 1; } Given that P holds at a call site, ESBMC deduces that Q holds upon return without re-examining the body; verification proceeds as assume(P ) → execute(f ) → assert(Q). Once f is verified to satisfy (P, Q, S), the contract replaces the implementation in any calling context. Function contracts serve two distinct roles in C ON V ER. In system-level verification (Replace mode), each call to f is substituted with an abstract stub abs(P, Q, s0 ) = { s | P (s0 ) ∧ Q(s0 , s) },
(1)
which havocs only the declared assigns targets and assumes Q; the internal state space is never explored. In functionlevel verification (Enforce mode), the real implementation is checked against (P, Q, S) by assuming P and asserting Q after execution. Enforce mode establishes the contract-conformance condition ∀s0 . P (s0 ) ⇒ Jf K(s0 ) ∈ abs(P, Q, s0 ),
(2)
i.e., the concrete execution trace of f is a witness in the abstract state set defined by the stub. Expanding (1) into (2)
reduces to the standard Hoare triple {P } f {Q}, which is precisely what ESBMC discharges during Enforce mode. A function that passes this check is contract-conformant. When both checks pass, soundness follows by substitution: because the real implementation satisfies (2), any property ϕ proved against the stub in Replace mode holds for the real code as well, and the composed result is end-to-end sound. b) Loop Invariants.: For programs containing loops, ESBMC supports the annotation of loop invariants via __ESBMC_loop_invariant() [23]. Unlike function contracts, which rely on deduction, loop invariants establish correctness through induction: a predicate is shown to hold before the loop begins, to be preserved by each iteration, and to imply the desired postcondition upon termination. Consider the following example: int sum = 0; for (int i = 0; i < n; i++) { __ESBMC_loop_invariant(sum == i * (i - 1) / 2); sum += i; } The invariant sum = ESBMC in three steps:
i(i−1) 2
is verified inductively by
1) Base case: the invariant holds at i = 0, since sum = . 0 = 0·(−1) 2 2) Inductive step: assuming the invariant holds at iteration i, after executing sum += i, we obtain sum′ = i(i−1) + 2 i(i+1) ′ i = 2 , which matches the invariant at i = i + 1. 3) Conclusion: when the loop exits at i = n, the invariant yields sum = n(n−1) . 2 This reduces an otherwise unbounded verification problem to a fixed inductive argument, avoiding loop unrolling entirely and sidestepping the state space explosion that would otherwise arise for large or non-terminating loops [24]. B. CEGAR+CEGIS a) Counterexample-Guided Abstraction Refinement (CEGAR): [4] drives the primary refinement loop in C ON V ER. Starting from LLM-derived contracts, each iteration runs two ESBMC checks: System-Level verification (function calls replaced by abstract contract stubs) and Function-Level verification (each implementation checked against its contract). If both pass, verification is sound by the assume-guarantee rule [25]. Otherwise, the counterexample is fed back to the LLM for contract refinement. Function-level failures direct the LLM to relax contracts; system-level failures direct it to strengthen them — reflecting that the two levels pull contracts in opposite directions. CEGAR runs for up to five iterations before escalating. An overview of CEGAR used in C ON V ER can be seen in Algorithm 2.
Algorithm 2 CEGAR Refinement in C ON V ER Require: Contracts C, results VS , VF , max iterations K Ensure: Refined ⟨C, VS , VF ⟩ 1: for k = 1 to K do 2: C ← C OUNTEREXAMPLE R EFINE(C, VS , VF ) 3: VS ← V ERIFY S YSTEM(P, C) 4: Vf ← V ERIFY F UNCTION(P, C, f ) for all f ∈ F 5: if PASS(VS ) ∧ ∀v ∈ VF : PASS(v) then 6: return ⟨C, VS , VF ⟩ 7: end if 8: if S TAGNANT(k) then 9: C ← D ELTA D EBUG(C) 10: break ▷ Escalate to CEGIS — Step 7 11: end if 12: end for 13: return ⟨C, VS , VF ⟩
b) Counterexample-Guided Inductive Synthesis (CEGIS): [26] serves as a second-stage fallback when CEGAR exhausts its budget. Counterexamples are classified and accumulated in a constraint database tracking positive examples (passing configurations), negative examples (states that must not satisfy the contract), and implication examples (inferred from observed program behaviour and structural patterns in the function body). Each synthesis call is conditioned on the full, accumulated constraint set, guiding the LLM toward contracts that are consistent with all observed behaviour. This loop also runs for up to five iterations; if the combined budget of up to ten iterations across both stages is exhausted without convergence, verification is declared inconclusive. Algorithm 3 describes how C ON V ER uses CEGIS. Algorithm 3 CEGIS Escalation in C ON V ER Require: Contracts C, results VS , VF , max iterations K Ensure: Refined ⟨C, VS , VF ⟩ 1: D ← CEGISDATABASE(VF ) ▷ Migrate counterexamples from CEGAR 2: for k = 1 to K do 3: C ← E XAMPLE S YNTHESIZE(C, D) ▷ Using Oracle 4: VS ← V ERIFY S YSTEM(P, C) 5: Vf ← V ERIFY F UNCTION(P, C, f ) for all f ∈ F 6: if PASS(VS ) ∧ ∀v ∈ VF : PASS(v) then 7: return ⟨C, VS , VF ⟩ 8: end if 9: Update D with new E + , E − from VF 10: end for 11: return ⟨C, VS , VF ⟩
C. SMART ICE a) ICE Learning.: C ON V ER structures verification feedback using the ICE framework [5], which classifies examples into three categories: positive examples (E + ) of states that must be included in the contract, negative examples (E − ) of
states that must be excluded, and implication examples encoding inductive relationships between states. Conflict detection identifies when a counterexample contradicts existing positive examples, keeping the database consistent. When ESBMC reports a failure, the raw output is parsed to extract the violated property and execution trace; tool-level failures are separated from semantic counterexamples, which are further classified into five categories — only unconstrained and semantic violations are admitted into E − , keeping the database free of noise. Algorithm 4 Counterexample Handling Pipeline - SMART ICE Require: Raw ESBMC output, current contracts, ICE database Ensure: Updated E + /E − /implications, weakest-link function 1: Parse output: extract violated property, trace, key variables 2: if tool-level failure (timeout / internal error / parse rejection) then 3: Record separately; exit 4: end if 5: Classify into: syntax error, unparsed, tool error, unconstrained init, semantic 6: if semantic or unconstrained initialisation then 7: Admit into E − 8: end if 9: if system-level failure then 10: Map variables → responsible functions 11: Compute gap score per function 12: Flag the highest-gap function as the weakest link 13: end if 14: Render structured diagnostic block (trace + E + /E − analysis) for LLM prompt
D. Pre-abstraction The pre-abstraction phase addresses the scalability limitation of compositional verification: certain functions exhibit structural complexity sufficient to trigger state explosion even at the function level. C ON V ER assigns each domain function a complexity score which is a weighted sum of static metrics extracted by regex analysis of the function body following established complexity metrics [27]. The weights reflect the cost model of BMC: loop count and nesting depth carry the highest per-occurrence weights because each iteration multiplies the path count. Recursion and unbounded loops incur large flat penalties, as a single occurrence renders the state space potentially infinite. Dynamic allocation is penalised moderately (bounded by calling context); branching and pointer operations contribute smaller per-occurrence costs. The score maps each function to one of four explosion-risk tiers: minimal (< 5.0), low (≥ 5.0), medium (≥ 10.0), and high (≥ 20.0). Functions in the medium or high tier (score ≥ 10.0, configurable) are designated for over-approximate abstraction; the rest undergo standard precise-contract synthesis. The LLM prompt for abstraction instructs the model to produce sound
but loose contracts: weaker postconditions (null-safety, range bounds) rather than full behavioural specifications, and an over-approximate assigns clause covering all globals that might be modified. A heuristic fallback generates tautological ensures clauses and a body-scan-derived assigns list when the LLM fails or produces unparseable output. The pipeline then proceeds through five phases: • Phase 1a: Generate over-approximate abstractions for high-complexity functions. • Phase 1b: Concurrently synthesise precise contracts for low-complexity functions via coverage-validated LLM derivation. • Phase 2: Run an initial ESBMC system-level check using the abstractions as function summaries, yielding a fast over-approximate verification result. • Phase 3: Verify each function atomically against its own contract (proceeds unconditionally, regardless of Phase 2 outcome). • Phase 4: Replace each successfully verified abstraction with its precise contract; unverified functions retain their conservative abstraction. • Phase 5: Escalate to CEGAR/CEGIS refinement if the substituted contracts still fail to establish the system property. This stratified strategy — abstract first, verify atomically, then refine — allows C ON V ER to handle programs that would otherwise be intractable under a single-phase compositional approach. V. B ENCHMARKS This Section describes the benchmarks that C ON V ER verifies. A. ESBMC-LF and LF-Hard To directly compare ConVer with tools that consume LF files, such as work from [17] which uses the LF Verfifier Benchmarks [28], a purpose-built preprocessor tool ESBMC-LF was created to convert the LF file benchmarks to C. ESBMC-LF translates the LF files into C with the verification conditions included, described in Algorithm 5. The purpose of the pipeline is to preserve the verification constructs of the LF benchmarks, which the LFC compiler strips from the converted code to ensure the compiled program runs efficiently. The resulting LF-Hard suite comprises 24 C programs converted from the LF Verifier Benchmarks [28]; further discussed in Section V-B. The remainder of Section V-A describes in further detail Algorithm 5. Steps 1–3 compile each LF benchmark to C via the LFC transpiler, normalize platform-dependent paths and compiler options, and combine all source files into a single translation unit. During combination, the reactor-c runtime library is replaced with a verification-friendly operational model that stubs the scheduler, event queue, and token lifecycle, so that ESBMC reasons only about the benchmark’s reaction logic. Steps 4–5 extract the Metric Temporal Logic (MTL) properties from the original LF source and encode them
as ESBMC verification constructs (__ESBMC_assert, __ESBMC_assume, and tracking variables) in the combined C file. Each MTL formula is pattern-matched to one of nine instrumentation templates that determine where assertions are placed and whether tracking variables are needed. Steps 6–7 generate a direct execution model that replaces the reactor-c scheduler. The pipeline parses the output topology to build a cascade graph; a static map from each reaction’s output port to its downstream reactions and emits direct function calls with is_present guards instead of runtime dispatch through trigger arrays. Loop bounds are derived from timer periods and property time horizons, yielding a finite, fully unrollable execution loop. Dead runtime infrastructure is then stripped to reduce the symbolic state space. Algorithm 5 ESBMC-LF: Converts LF files to C with verification property preservation Require: LF Benchmark B Ensure: C Program c file with property set Φ 1: Step 1: Semantic LF-to-C translation 2: P ← C OMPILE LF(B) ▷P is a C project semantically equivalent to B without MTL properties assuming LFC tool performs sound conversion 3: Step 2: Platform normalization 4: P ′ ← N ORMALIZE P ROJECT (P ) ▷ Resolve platform-dependent paths, headers, and definitions 5: Step 3: Single translation unit construction 6: C ← F LATTEN P ROJECT(P ′ , OM ) ▷ Replace runtime library with operational model OM , preprocess into one translation unit, filter system headers 7: Step 4: Property extraction 8: Φ ← E XTRACT MTL(B, C) ▷ Parse MTL annotations from B, map symbols to locations in C 9: Step 5: Property instrumentation 10: C ′ ← I NSTRUMENT MTL(Φ, C) ▷ Insert assertions, assumptions, and tracking variables per Φ 11: Step 6: Execution model generation 12: C ′′ ← G EN E XEC M ODEL(C ′ ) ▷ Build cascade graph from output topology, replace scheduler dispatch with direct calls, derive loop bounds 13: Step 7: Post-processing 14: c file ← P OST P ROCESS(C ′′ ) ▷ Strip dead runtime code, fix preprocessor-baked constants, propagate action values, remove line directives 15: return c file B. Benchmark Suites We evaluate C ON V ER on four alternative benchmark suites totalling 79 C programs, spanning algorithmic code, loop and recursion intensive verification challenges, and real-world parsing routines. a) LF2C-Simple (17 Programs).: These LF2C-Simple Benchmarks were synthesised using Claude 3.5 Sonnet [29]. Where the LLM was prompted with the original LF Benchmark with the explicit instruction to generate a semantically
equivalent C Program version with the system property inserted at the correct position inside the code. We successfully obtained 17 of the 24 benchmarks; the remainder contained buggy cases that led to Verification Failed due to a logic error injected by the LLM, and we were unable to verify the system property. b) Frama-C (45 programs).: Drawn from a FramaC/ACSL exercise set used to evaluate deductive verification tools at FM 2026-AE [20], the suite covers numerical computations, array operations, sorting, and searching (e.g., add, sort, binary_search). Original ACSL annotations (//@ requires/ensures) are removed, and the same property is re-expressed as a single top-level assert() in main(). Programs are typically under 100 LOC, making this suite well-suited for evaluating the core CEGAR plus ICE contract synthesis pipeline on well-structured algorithmic code without structural interference. c) VerifyThis (11 programs).: Drawn from three SV-COMP [30] categories — six from the VerifyThis track (lcp, prefixsum, prefixsum_rec, duplets, elimination_max_rec, elimination_max_rec_onepoint), two from recursive-simple (fibo, sum), and three from recursive (MultCommutative, EvenOdd, Addition) — the programs are adapted by replacing dynamic memory allocation with fixed-size stack arrays and reducing verification bounds (e.g., n ≤ 8 for prefix sum, n ≤ 6 for elimination max) to prevent state-space explosion. Four programs were excluded: elimination_max has a monolithic main() with no callee, and three tree-manipulation programs (tree_del_iter, tree_del_rec, tree_max) require heap-allocated structures with ∀-quantified postconditions unsupported by __ESBMC_ensures. The suite is evaluated exclusively with the Pre-Abstraction strategy, as loop-intensive programs cause state-space explosion under direct synthesis and recursive programs exceed SmartICE’s capacity without prior abstraction. d) X.509 (6 programs).: Extracted from the ANSSI-FR x509-parser project and included in the same FM 2026 artifact [20] as the Frama-C suite, these programs implement real-world ASN.1/X.509 routines: buffer comparison (bufs_differ), IA5 string validation (check_ia5_string), ASN.1 type parsers (parse_null, parse_algoid_params_none), time-field encoding (time_components_to_comparable_u64), and time field checking (verify_correct_time_use). Three adaptations are applied for ESBMC compatibility: (1) static qualifiers are removed (required for --enforce-contract to locate functions by name); (2) ACSL assertions are replaced with C assert(); and (3) universal quantifiers are encoded via a nondet index—e.g., \forall integer i; 0<=i<len ==> buf[i]<=0x7f becomes:
TABLE I E XPERIMENTAL SETUP. Parameter
Value
ESBMC version LLM backends
8.1.0 Qwen3.5-Plus; Haiku 4.5; OSS 120b 5 600 s 900 s 3/1
Max iterations Timeout (Frama-C / Simple / X.509) Timeout (VerifyThis) Workers (cloud / local)
GPT-
u32 idx; __ESBMC_assume(idx < len); if (ret == 0) assert(buf[idx] <= 0x7f);
ESBMC’s BMC engine explores all nondet values of idx, making this encoding semantically equivalent to the universal quantifier within the bounded path. Ranging from singlefunction leaf parsers to three-level call chains with pointer arithmetic, this suite is substantially harder than the Frama-C benchmark and probes whether C ON V ER’s CEGAR+ICE loop can synthesise sound pointer contracts for low-level code. VI. E XPERIMENTS a) Tool and hardware configuration.: All experiments use ESBMC 8.1.0 as the backend verifier and perform at most 5 CEGAR iterations per program. We evaluate three LLM backends: Qwen-Plus (DashScope cloud API), Claude Haiku 4.5 (Anthropic cloud API), and GPT-OSS 120b served locally via Ollama on a server with four NVIDIA RTX A6000 GPUs (48 GB each). Table I summarises the parameters. For the Frama-C benchmark, LF2C-Simple, and X.509 we set a per-program timeout of 600 s and run three workers in parallel for cloud models (one for GPT-OSS 120b). For VerifyThis, we extend the timeout to 900 s to accommodate deeper recursion and loop complexity. b) Strategies.: We compare two verification strategies: SmartICE applies the full CEGAR+SMART ICE pipeline with structured counterexample feedback, while No-ICE disables ICE learning and serves as an ablation baseline. Both strategies are applicable to the Frama-C benchmark, LF2C-Simple, and X.509, which consist of short programs with explicit functioncall structure. For VerifyThis — programs with deep or unbounded recursion that cause state explosion under direct synthesis — we apply the Pre-Abstraction strategy exclusively. A. Results on Function-Contract Benchmarks (RQ1) Table II shows verification outcomes on Frama-C benchmark (45 programs), LF2C-Simple (17 programs), and X509 (6 programs) using the SmartICE strategy. Figure 3 provides a visual overview across all four benchmarks. C ON V ER achieves strong results on the Frama-C benchmark: GPT-OSS 120b converges on 43 of 45 programs (96%), Qwen-Plus on 40 (89%), and Claude Haiku 4.5 on 37 (82%). Across LF2C-Simple, which compiles the same LF programs into C and runs them through the same pipeline, results
TABLE II V ERIFIED PROGRAMS (S MART ICE STRATEGY ) ON THE F RAMA -C BENCHMARK , LF2C-S IMPLE , AND X509. N UMBERS SHOW CONVERGED / TOTAL (%). Q WEN = Q WEN -P LUS ; C LAUDE = H AIKU 4.5; GPT = GPT-OSS 120 B .
Benchmark Frama-C (45) LF2C-Simple (17) X509 (6) 50
Qwen
Claude
GPT-OSS
40 (89%) 14 (82%) 3 (50%)
37 (82%) 14 (82%) 3 (50%)
43 (96%) 15 (88%) 2 (33%)
FM2026 Benchmark Results 3 Models × 2 Strategies 89%
87%
82%
87%
96%
91%
Programs (out of 45)
40 30 20 Converged (both levels) System-only Failed Timeout No-ICE (hatched)
10 0
Qwen3.5-Plus SmartICE
Qwen3.5-Plus No-ICE
Haiku 4.5 SmartICE
Haiku 4.5 No-ICE
GPT-OSS SmartICE
GPT-OSS No-ICE
Fig. 2. Outcome breakdown on Frama-C benchmark (45 programs) for three LLM backends and two strategies. Stacked bars show counts for converged (green), system-only (orange), failed (red), and timeout (grey).
are consistent at 82–88%. The X509 benchmark is markedly harder: these programs contain pointer-heavy certificate parsing code, and the 33–50% convergence rate reflects the difficulty of generating sound pointer contracts for low-level memory operations with current LLMs. Figure 2 breaks down outcomes (converged, system-only, failed, timeout) by model and strategy on the Frama-C benchmark. The Frama-C benchmark results reveal a clear dominance of first-iteration convergence across all three models. For GPTOSS 120b, 40 of the 43 converged programs (93%) require only a single CEGAR iteration; the remaining three converge at iteration 2. Figure 4 shows the full iteration distribution. a) RQ1 — Verification effectiveness.: C ON V ER achieves 82–96% on Frama-C benchmark and LF2C-Simple, with a narrow spread across three backends, suggesting the CEGAR+ICE loop is largely model-agnostic for wellstructured algorithmic programs. X509 (33–50%) is the outlier: pointer-heavy certificate parsing exposes a gap in current LLM contract synthesis for low-level memory code that no backend closes. B. ICE Learning Ablation (RQ2) To isolate the contribution of SMART ICE learning, we compare SmartICE and No-ICE on the Frama-C benchmark for all three backends. Figure 5 visualises the comparison. The ablation reveals a picture more nuanced than a simple verdict on ICE. GPT-OSS 120b gains the most from structured counterexample feedback (+2 programs, 96% vs. 91%), and
Qwen-Plus benefits similarly (+1 program, 89% vs. 87%). Claude Haiku 4.5 tells a different story: it converges on two fewer programs under SmartICE (37/45) than without it (39/45). The divergence has a traceable cause. The value of an ICE database depends entirely on the informational quality of its entries: a negative example is useful only if it captures a genuine semantic property of the failed contract, not a surface artefact of how the contract was written. For Claude Haiku 4.5, two failure modes corrupt this signal. First, when the model produces a syntactically ill-formed contract—such as using a boolean literal in a context where ESBMC expects a C integer expression—the resulting parse error is stored as a negative example, and the ICE loop constrains subsequent refinement away from that surface pattern. The model responds by producing other malformed expressions rather than resolving the underlying cause, trapping the loop until the iteration budget expires. Second, when ESBMC emits counterexamples in a format that ConVer’s parser cannot decode, those semantically empty entries populate the E− database and are presented back to the model as though they carried structural meaning— noise wearing the appearance of signal. Larger backends, by contrast, generate syntactically well-formed contracts more reliably and elicit richer, more structured ESBMC witnesses, keeping their counterexample databases clean and the feedback loop genuinely informative. ICE, in this light, functions as a capability amplifier: it sharpens refinement precisely where the LLM already generates high-quality artefacts, and offers diminishing—or in the extreme, negative—returns where those artefacts are noisier. a) RQ2 — ICE learning contribution.: SMART ICE learning yields its strongest gains for the highestcapability backend, lifting GPT-OSS 120b by five percentage points (96% vs. 91%) and Qwen-Plus by two (89% vs. 87%). Claude Haiku 4.5, whose smaller capacity leads to more frequent contract syntax errors and less structured ESBMC witnesses, does not benefit: its ICE database accumulates noise rather than signal, and the feedback loop becomes counterproductive. The finding reframes the role of ICE: rather than a uniform improvement over pure CEGAR, it is a capability-conditioned amplifier— most valuable precisely where the LLM is already strong enough to generate artefacts from which structured feedback can be meaningfully extracted. C. Results on Complex Programs (RQ3) LF-Hard Benchmarks (24 programs): Table III shows results on the 24 LF-Hard benchmarks (1,998–4,328 LOC each) under the Pre-Abstraction strategy with a 600 s budget. Figure 6 visualises the outcome breakdown. Direct ESBMC without contracts verifies 10 of 24 programs within budget, providing a baseline: these are already simplified C translations of LF reactor models that ESBMC can handle monolithically. C ON V ER improves on this across all
ConVer Benchmark Overview (best strategy per benchmark type) Qwen3.5-Plus
40/45 SmartICE
14/17 SmartICE
3/6 SmartICE
6/11 Preabs
11/24 Preabs
Haiku 4.5
37/45 SmartICE
14/17 SmartICE
3/6 SmartICE
7/11 Preabs
12/24 Preabs
GPT-OSS 120b
43/45 SmartICE
15/17 SmartICE
2/6 SmartICE
6/11 Preabs
15/24 Preabs
Frama-C (45)
LF2C-Simple (17)strategy SmartICE
X.509 (6)
VerifyThis LF-Hard (11) (24) Preabs strategy
80 60 40 20
Convergence rate (%)
100
0
Fig. 3. Verification success rate (%) across all four benchmarks and three LLM backends. Each cell shows the convergence percentage under the best applicable strategy for that benchmark.
CEGAR Iteration Distribution FM2026, SmartICE
Programs
95%
35 30 25 20 15 10 5 0
Qwen3.5-Plus (40/45 converged)
35
92%
Haiku 4.5 (37/45 converged)
GPT-OSS 120b (43/45 converged)
25
15
20 10
1
2
3
CEGAR Iteration
7%
8%
0
4
14%
5
5
2%
30%
10
15
2%
49%
20
30
1
2
3
CEGAR Iteration
4
0
1
2
3
CEGAR Iteration
4
Fig. 4. CEGAR iteration distribution on Frama-C benchmark (SmartICE) for three LLM backends. Nearly all converged programs require only a single iteration.
Converged programs (out of 45)
50 40
SmartICE vs No-ICE Ablation FM2026 SmartICE (solid) No-ICE (hatched)
88%
86%
95% 82%
86%
91%
TABLE III P RE -A BSTRACTION RESULTS ON LF-H ARD BENCHMARKS (24 PROGRAMS , 600 S BUDGET ). “D IRECT ESBMC” VERIFIES WITHOUT CONTRACTS ; C ON V ER COLUMNS USE P RE -A BSTRACTION . Q WEN = Q WEN -P LUS ; C LAUDE = H AIKU 4.5; GPT = GPT-OSS 120 B .
30
Converged Timeout Failed
20 10 0
Qwen3.5-Plus
Haiku 4.5
GPT-OSS 120b
Fig. 5. SmartICE vs. No-ICE on the Frama-C benchmark for three LLM backends. Each pair of bars shows converged program counts with and without ICE learning.
three backends: GPT-OSS 120b leads at 15/24 (62%), followed by Claude Haiku 4.5 at 12/24 (50%) and Qwen-Plus at 11/24 (46%). The gains stem from programs such as Election, ADASModel, and ProcessMsg where monolithic ESBMC exploration times out, but contract-based decomposition reduces each function-level SMT instance to a tractable size.
Direct ESBMC
Qwen3.5-Plus
Haiku4.5
GPT-OSS
10 (42%) 14 0
11 (46%) 12 1
12 (50%) 11 1
15 (62%) 8 1
GPT-OSS 120b additionally converges on Fibonacci and TrainDoorFeedback where the smaller models time out, reflecting higher contract synthesis quality from the larger model. The ordering of results mirrors the model’s capability, confirming that contract synthesis quality, not ESBMC’s solving capacity, is the binding constraint on these benchmarks. Most converged programs require no CEGAR refinement (iteration 0); the few that do (e.g., Election at iter=1, Fibonacci at iter=2 for GPT-OSS 120b) converge quickly, indicating the refinement loop is effective when initial contracts are close to correct. ProcessSync is the single FAILED program across all
LF-Hard Benchmarks (24 programs, 600 s budget)
Programs (out of 24)
24
18
42%
46%
50%
14
12
11
10
11
12
1
1
62%
1 8
12
6
Converged
Timeout
Qwen-Plus (ours)
Claude Haiku (ours)
15 Failed
0 Direct ESBMC
GPT-OSS 120b
Fig. 6. Outcome breakdown on LF-Hard benchmarks (24 programs, 600 s budget). Direct ESBMC (42%) is the no-contract baseline. GPT-OSS 120b leads at 62%, with Claude Haiku 4.5 at 50% and Qwen-Plus at 46%, confirming that stronger contract synthesis yields higher convergence. TABLE IV P RE -A BSTRACTION STRATEGY RESULTS ON V ERIFY T HIS (900 S TIMEOUT ). Q WEN = Q WEN -P LUS ; C LAUDE = H AIKU 4.5; GPT = GPT-OSS 120 B .
Benchmark VerifyThis (11)
Qwen3.5-Plus
Haiku4.5
GPT
6 (55%)
7 (64%)
6 (55%)
LLM backends; ESBMC rejects its structure at the systemlevel check before contract synthesis begins, so it is excluded from the convergence count. VerifyThis Benchmarks (11 programs): For VerifyThis (11 recursive and loop-invariant programs), we apply the PreAbstraction strategy. Table IV summarises the outcomes. On VerifyThis, Claude Haiku 4.5 achieves 7/11 (64%), matching the reference result produced by the pipeline authors under manual configuration. Qwen-Plus and GPT-OSS 120b both reach 6/11 (55%). The four programs that fail across all backends — MultCommutative, duplets, prefixsum, and prefixsum_rec — involve complex inter-procedural invariants that exceed the current contract synthesis capability within the iteration budget. a) RQ3 — Performance on complex programs.: On LF-Hard (24 programs), Pre-Abstraction lifts convergence from 42% (direct ESBMC) to 62% (GPT-OSS 120b), with results ordering by model capability (GPT-OSS 120b > Claude > Qwen), confirming that contract synthesis quality is the binding constraint. On VerifyThis (11 programs), Pre-Abstraction achieves 55–64%, with Claude Haiku 4.5 matching the expert reference at 7/11; the four failing programs involve complex inter-procedural invariants beyond current synthesis capability. VII. D ISCUSSION a) Comparison with state of the art.: The most closely related tool is P OLY V ER [17], which also applies LLM-based
contract synthesis in a CEGIS–CEGAR loop to verify Lingua Franca programs. The two systems are complementary rather than directly competing. P OLY V ER operates at the LF source level: each benchmark comprises 18–206 LOC of LF source and 2–64 LOC of C reaction code, and UCLID5 is used as the system-level model checker, enabling verification of temporal properties expressed as extended state machines and support for polyglot (C and Rust) reactions. C ON V ER operates on the fully translated C output of ESBMC-LF, where the same benchmarks expand to 1 998–4 328 LOC monolithic C files including the complete LF runtime. This makes C ON V ER’s verification task substantially harder—state explosion in the translated code is why direct ESBMC fails on 14 of 24 benchmarks—but it also makes C ON V ER independent of any LF-specific toolchain: it verifies standard C programs without requiring a separate model-checking frontend. Where P OLY V ER achieves 22/22 on its benchmark set at the source level, C ON V ER achieves 15/24 (GPT-OSS 120b) on the translated-C versions of the same programs, overall 16/24 across all run-throughs, a result that is not directly comparable but highlights the additional challenge of verifying runtimeinclusive translations. ACSE [20] is evaluated on the same Frama-C and X.509 benchmarks used in this paper, making it a direct point of comparison. ACSE generates ACSL pre/post-conditions and assigns clauses via array-carrying symbolic execution, and crucially supports quantified loop invariants (e.g., ∀i. a[i] ≥ 0) through its symbolic segment abstraction. C ON V ER does not generate quantified invariants: ESBMC’s function contract mechanism does not support first-order quantifiers in requires/ensures clauses, so the Frama-C benchmark is restricted to the 45 programs whose properties can be expressed without quantification. Programs that require quantified array invariants are outside C ON V ER’s current scope, and ACSE handles these cases where C ON V ER cannot. Within the quantifier-free subset, C ON V ER’s CEGAR loop provides a complementary advantage: rather than inferring contracts analytically in a single pass, it iteratively refines contracts against formal counterexamples, which handles cases where symbolic invariant inference is imprecise or the program is too large for exhaustive symbolic exploration. b) Persistent system-only cases.: Across all four configurations, 4–5 programs reach the system-only outcome: the system-level ESBMC check passes, but at least one functionlevel check fails within the iteration limit. Inspection reveals that these programs contain loop-heavy functions for which the LLM consistently produces contracts that are too strong for the implementation to satisfy, and the 5-iteration budget is insufficient to relax them to a valid specification. Increasing the iteration limit or adding an automatic loop invariant synthesis step for these functions are promising remedies. c) Threats to validity.: Three threats apply. First, the Frama-C benchmark consists entirely of relatively simple single-assertion programs; generalisation to multi-property, multi-function programs remains to be demonstrated. Second, LLM outputs are stochastic, so results may vary across
runs; we ran each configuration once and have not yet conducted repeated-trial experiments. Third, the one known soundness caveat is specific to ESBMC’s assigns clause implementation: pointer-dereference targets (e.g., assigns *instance_args) are not currently supported by ESBMC and are stripped from contracts before invocation, so frame conditions for state modified through pointer parameters are not mechanically verified. This is a limitation of the ESBMC backend, not of the compositional method: all requires, ensures, and scalar assigns clauses are verified normally, and the method’s soundness argument holds for the verified portion of each contract. All results reported in the tables are valid under these conditions. VIII. C ONCLUSION We have presented C ON V ER, a tool for LLM-guided topdown compositional verification of C programs using ESBMC function contracts. On the Frama-C benchmark of 45 C programs, C ON V ER achieves 82–96% verification success across three LLM backends (GPT-OSS 120b 96%, Qwen-Plus 89%, Claude Haiku 4.5 82%), with over 93% of converged programs requiring only a single CEGAR iteration. On LF2C-Simple (17 programs) results are consistent at 82–88%, confirming that the pipeline generalises beyond its primary benchmark. On the VerifyThis suite of 11 recursive and loop-intensive programs, the Pre-Abstraction strategy achieves 55–64%, with Claude Haiku 4.5 matching the expert reference at 7/11. All three backends achieve competitive results on well-structured programs, while on harder benchmarks (LF-Hard, 46–62%) results correlate with model capability, confirming that the CEGAR+ICE loop is the primary driver of convergence on tractable programs. Future work will target two directions: (1) extending the approach to programs with multiple top-level assertions, and (2) investigating hybrid model selection strategies that route simple programs to fast, cheap LLMs and complex programs to stronger reasoning models. IX. ACKNOWLEDGEMENTS The authors of this research disclose that generative AI was used in the development of the tooling and in the execution of the methodological evaluation. After using these tool(s)/service(s), the author(s) reviewed and edited the content as needed and take(s) full responsibility for the publication’s content. AVAILABILITY The C ON V ER tool, all benchmark programs, pre-computed experiment results, and reproduction scripts are openly available as a replication package on Zenodo at https://doi.org/ 10.5281/zenodo.19249204. The artifact includes the C ON V ER source code, ESBMC v8.1 static binary, all four benchmark suites (Frama-C, X.509, LF2C-Simple, VerifyThis, LF-Hard), and the figures and notebooks used to generate the results in this paper.
R EFERENCES [1] T. Wu, X. Li, E. Manino, R. S. Menezes, M. R. Gadelha, S. Xiong, N. Tihanyi, P. Petoumenos, and L. C. Cordeiro, “Esbmc v7. 7: Efficient concurrent software verification with scheduling, incremental smt and partial order reduction: (competition contribution),” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2025, pp. 223–228. [2] N. Chong, B. Cook, J. Eidelman, K. Kallas, K. Khazem, F. R. Monteiro, D. Schwartz-Narbonne, S. Tasiran, M. Tautschnig, and M. R. Tuttle, “Code-level model checking in the software development workflow at amazon web services,” Software: Practice and Experience, vol. 51, no. 4, pp. 772–797, 2021. [3] E. M. Clarke, W. Klieber, M. Nováček, and P. Zuliani, “Model checking and the state explosion problem,” in LASER Summer School on Software Engineering. Springer, 2011, pp. 1–30. [4] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexampleguided abstraction refinement,” in International Conference on Computer Aided Verification. Springer, 2000, pp. 154–169. [5] P. Garg, C. Löding, P. Madhusudan, and D. Neider, “Ice: A robust framework for learning invariants,” in International Conference on Computer Aided Verification. Springer, 2014, pp. 69–87. [6] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without bdds,” in International conference on tools and algorithms for the construction and analysis of systems. Springer, 1999, pp. 193–207. [7] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, “Bounded model checking.” Handbook of satisfiability, vol. 185, no. 99, pp. 457– 481, 2009. [8] L. Cordeiro and B. Fischer, “Bounded model checking of multi-threaded software using smt solvers,” arXiv preprint arXiv:1003.3830, 2010. [9] M. R. Gadelha, F. R. Monteiro, J. Morse, L. C. Cordeiro, B. Fischer, and D. A. Nicole, “Esbmc 5.0: an industrial-strength c model checker,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 888–891. [10] R. S. Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brauße, M. R. Gadelha, N. Tihanyi et al., “Esbmc v7. 4: Harnessing the power of intervals: (competition contribution),” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2024, pp. 376–380. [11] H. Jelodar, S. Bai, P. Hamedi, H. Mohammadian, R. Razavi-Far, and A. Ghorbani, “Large language model (llm) for software security: Code analysis, malware analysis, reverse engineering,” Journal of Information Security and Applications, vol. 98, p. 104390, 2026. [12] C. S. Xia, Y. Wei, and L. Zhang, “Automated Program Repair in the Era of Large Pre-trained Language Models,” in 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). Melbourne, Australia: IEEE, May 2023, pp. 1482–1494. [Online]. Available: https://ieeexplore.ieee.org/document/10172803/ [13] J. Liu, S. Xie, J. Wang, Y. Wei, Y. Ding, and L. Zhang, “Evaluating Language Models for Efficient Code Generation,” Aug. 2024, arXiv:2408.06450. [Online]. Available: http://arxiv.org/abs/2408.06450 [14] N. Tihanyi, Y. Charalambous, R. Jain, M. A. Ferrag, and L. C. Cordeiro, “A new era in software security: Towards self-healing software via large language models and formal verification,” in 2025 IEEE/ACM International Conference on Automation of Software Test (AST). IEEE, 2025, pp. 136–147. [15] F. Zubair, M. Al-Hitmi, and C. Catal, “The use of large language models for program repair,” Computer Standards & Interfaces, vol. 93, p. 103951, Apr. 2025. [Online]. Available: https://www.sciencedirect. com/science/article/pii/S092054892400120X [16] M. Haque, P. Babkin, F. Farmahinifarahani, and M. Veloso, “Towards Effectively Leveraging Execution Traces for Program Repair with Code LLMs,” May 2025, arXiv:2505.04441 [cs] version: 1. [Online]. Available: http://arxiv.org/abs/2505.04441 [17] P.-W. Chen, S. Lin, A. Godbole, R. Singh, E. Polgreen, E. Lee, and S. Seshia, “Polyver: A compositional approach for polyglot system modeling and verification,” 2025. [Online]. Available: https: //repositum.tuwien.at/handle/20.500.12708/219538 [18] Z. Wang, T. Lin, M. Chen, H. Li, M. Yang, X. Yi, S. Qin, Y. Luo, X. Li, B. Gu et al., “A tale of 1001 loc: Potential runtime errorguided specification synthesis for verifying large-scale programs,” arXiv preprint arXiv:2512.24594, 2025. [19] S. A. Seshia and P. Subramanyan, “Uclid5: integrating modeling, verification, synthesis and learning,” in 2018 16th ACM/IEEE International
Conference on Formal Methods and Models for System Design (MEMOCODE). IEEE, 2018, pp. 1–10. [20] W. Lu, J. Ke, H. Fu, Z. Sun, Y. Zhou, G. Li, and H. Li, “Array-carrying symbolic execution for function contract generation,” in Proceedings of the 26th International Symposium on Formal Methods (FM 2026), ser. Lecture Notes in Computer Science. Springer, 2026. [21] A. Zeller, “Yesterday, my program worked. today, it does not. why?” ACM SIGSOFT Software engineering notes, vol. 24, no. 6, pp. 253–267, 1999. [22] A. Zeller and R. Hildebrandt, “Simplifying and isolating failure-inducing input,” IEEE Transactions on software engineering, vol. 28, no. 2, pp. 183–200, 2002. [23] R. Sá Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brauße, M. R. Gadelha, N. Tihanyi, K. Korovin, and L. C. Cordeiro, “ESBMC 7.4: Harnessing the power of intervals,” Systems & Software Verification Laboratory, Software Documentation, 2024, version 7.4. Available at: https: //github.com/esbmc/esbmc. Accessed: 2026-03-20. [Online]. Available: https://esbmc.github.io/docs/#quantifiers [24] M. A. Pirzada, G. Reger, A. Bhayat, and L. C. Cordeiro, “Llm-generated invariants for bounded model checking without loop unrolling,” in Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024, pp. 1395–1407. [25] A. Komuravelli, C. S. Păsăreanu, and E. M. Clarke, “Assume-guarantee abstraction refinement for probabilistic systems,” in International conference on computer aided verification. Springer, 2012, pp. 310–326. [26] A. Solar-Lezama, C. G. Jones, and R. Bodik, “Sketching concurrent data structures,” in Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’08. New York, NY, USA: Association for Computing Machinery, 2008, p. 136–148. [Online]. Available: https://doi.org/10.1145/1375581.1375599 [27] T. J. McCabe, “A complexity measure,” IEEE Transactions on software Engineering, no. 4, pp. 308–320, 1976. [28] S. Lin, Y. A. Manerkar, M. Lohstroh, E. Polgreen, S.-J. Yu, C. Jerad, E. A. Lee, and S. A. Seshia, “Towards building verifiable cps using lingua franca,” ACM Transactions on Embedded Computing Systems, vol. 22, no. 5s, pp. 1–24, 2023. [29] Anthropic, “Introducing Claude 3.5 Sonnet,” 2024, accessed: 2026-03-27. [Online]. Available: https://www.anthropic.com/news/ claude-3-5-sonnet [30] D. Beyer, “State of the art in software verification and witness validation: Sv-comp 2024,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2024, pp. 299–329.