一句话：在 Iris 中构建基于 CompCert 语义的分离逻辑实例，以验证 C 程序正确性。
Iris 是通用分离逻辑框架，已有实例多基于简单核心演算，难以直接推理实际语言程序。本文基于经过验证的 C 编译器 CompCert 开发 Iris 实例，使 C 程序在编译运行所用语义下得到正确性证明。作者借鉴 Verified Software Toolchain（VST）的 CompCert C 分离逻辑，将其程序逻辑在 Iris 中重新实现。由于 Iris 默认的资源模型和最弱前置条件/Hoare 三元组定义不能直接套用于 CompCert，本文提出适配 CompCert 内存的新资源模型，并重新定义最弱前置条件与 Hoare 三元组。最终在 Iris 内获得完整的 CompCert C 程序逻辑，并重建 VST 顶层自动化的一部分，用于证明简单 C 程序正确。
Iris is a generic separation logic framework that has been instantiated to reason about a wide range of programming languages and language features. Most Iris instances are defined on simple core calculi, but by connecting Iris to new or existing formal semantics for practical languages, we can also use it to reason about real programs. In this paper we develop an Iris instance based on CompCert, the verified C compiler, allowing us to prove correctness of C programs under the same semantics we use to compile and run them. We take inspiration from the Verified Software Toolchain (VST), a prior separation logic for CompCert C, and reimplement the program logic of VST in Iris. Unlike most Iris instances, this involves both a new model of resources for CompCert memories, and a new definition of weakest preconditions/Hoare triples, as the Iris defaults for both of these cannot be applied to CompCert as is. Ultimately, we obtain a complete program logic for CompCert C within Iris, and we reconstruct enough of VST’s top-level automation to prove correctness of simple C programs.