一句话：COHEC 把堆约束求解重构为「LLM 提议堆模型 + 可信验证器验证」，显著提升混合执行的路径探索与取值生成能力。
面向对象程序的混合执行中，空值性、别名、运行时类型与字段可达性等堆约束要求构造具体堆模型，现有 SMT 引擎与符号堆技术难以有效处理，构成实际瓶颈。作者提出 COHEC：将路径条件分解为原始部分（由 SMT 求解）与堆部分（由堆约束求解器 HCS 处理）；HCS 让 LLM 提出候选堆模型与初始化代码，再由可信验证器执行校验，仅接受确实满足全部约束的模型，从而把 LLM 排除在可信基之外。系统在 JDart/JPF 上实现，于十个 Java 库的 6750 个 API 及 commons-lang3 分层样本上与 CONCOLLMIC 对比：相比原生 JDart 显著提升路径探索与具体取值生成，且比 CONCOLLMIC 覆盖率更高、时间与 token 开销更低。
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.
@inproceedings{paperbot12520,
title = {Verifier-in-the-Loop LLM Solving of Heap Constraints for Concolic Execution},
author = {Shaoran Xia and Leyi Cheng and Caihua Dong and Dongdong She and Bo Wang and Xin Peng and Zhen Dong},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834410}
}