Verifier-in-the-Loop LLM Solving of Heap Constraints for Concolic Execution

Abstract

Concolic execution systematically explores program paths by solving symbolic constraints, but in object-oriented software its practical effectiveness is often limited by heap constraints over objects and heap structure, such as nullness, aliasing, runtime types, and field reachability. These constraints form a systematic bottleneck in real-world software because satisfying them requires constructing a concrete heap model rather than merely computing primitive valuations, which existing SMT-based concolic engines and symbolic heap techniques do not handle effectively. We present COHEC, a hybrid concolic architecture that decomposes each target path condition into a primitive component solved by an SMT solver and a heap component handled by a Heap Constraint Solver (HCS). Given extracted heap constraints, HCS uses an LLM to propose candidate heap models and initialization code, while a trusted verifier executes and verifies the generated code, admitting only models whose initialization code constructs states that satisfy all constraints and keeping the LLM outside the trusted computing base. We implement COHEC on top of JDart/JPF and evaluate it on 6,750 APIs from ten Java libraries, together with a stratified sample from commons-lang3 against the LLM-assisted baseline CONCOLLMIC. The results show that COHEC substantially improves path exploration and concrete valuation generation over native JDart, while achieving higher coverage than CONCOLLMIC at lower time and token cost. Overall, the findings indicate that treating heap constraint solving as verified heap model construction is a practical and effective way to extend concolic execution to the object-sensitive behaviors pervasive in modern software.