一句话：提出 imaginary specifications，将可执行代码与所有权断言自由混合，并构建 CRIS 框架推广 CCR，支持对未验证代码副作用的模块化推理。
CCR 框架统一了 refinement 与分离逻辑，可在包含未验证代码的开放环境中提供基于所有权的模块化推理与传递式增量推理。然而，在推理函数调用时，客户端可用的推理原则仍局限于前后条件，难以刻画 I/O 动作或与任意未验证代码交互等 effectful 行为，这一问题在混合验证中尤为尖锐——不同验证技术混用，部分代码从未被形式验证而仅经测试或模型检测。为此，论文提出 imaginary specifications：一种将可执行代码与所有权断言自由混合的新概念，并给出其使用所需的推理原则。通过若干关键技术发展，作者提出 CRIS（Contextual Refinement with Imaginary Specifications），将 CCR 推广至支持 imaginary specifications。论文用涉及未验证代码、含 I/O 或发散等任意副作用的混合验证示例展示了 CRIS 的表达力与推理能力，并在 Rocq 中完成完整机器化。
The CCR framework unifies refinement and separation logic to provide ownership-based modular reasoning and transitive incremental reasoning in open settings that involve unverified code. However, when reasoning about function invocations, the reasoning principles available to clients remain confined to pre- and postconditions, which struggle to capture effectful behaviors such as I/O actions or interactions with arbitrary unverified code. This limitation becomes particularly acute in hybrid verification , where a mixture of different verification techniques is applied and some code is never formally verified but instead tested or model-checked. To overcome this limitation, we introduce imaginary specifications —a novel notion that freely mixes executable code with ownership assertions—and reasoning principles for their use. Through key technical developments, we present CRIS (Contextual Refinement with Imaginary Specifications), a framework that generalizes CCR with support for imaginary specifications. We demonstrate CRIS’s expressiveness and reasoning power through examples involving hybrid verification with unverified code exhibiting arbitrary side effects such as I/O or divergence, with complete mechanization in Rocq.
@article{KimYYLMHLRINKH26,
title = {CRIS: The Power of Imagination in Hybrid Verification},
author = {Yonghee Kim and Taeyoung Yoon and Sanghyun Yi and Jaehyung Lee and Soonwon Moon and Yeji Han and Seonho Lee and Taeyoung Rhee and Yujin Im and Donghyun Nam and Jieung Kim and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808317}
}