一句话：提出 Archmage 内存模型框架及 CompCertCast 编译链与源级逻辑，首次实现含整数-指针转换程序的实用端到端验证。
现有支持整数-指针转换的形式化内存模型并非为端到端验证设计，既无法支持某些重要的源级编码模式、难以论证部分后端优化，也缺少用于程序验证的源级逻辑。本文提出 Archmage：一个面向端到端验证的整数-指针转换框架，支持广泛的源级编码模式、后端优化，并给出形式化的 out-of-memory 概念。基于 Archmage，作者构建了 CompCertCast——将 Archmage 接入 CompCert 的扩展，为含整数-指针转换的程序提供完整经验证的编译链；同时提出 Archmage logic——用于推理整数-指针转换的源级逻辑。设计上缓解了形式化支持带来的开销，并通过验证一个基于 xor 的链表实现展示该逻辑的有效性。该工作给出了首个实用的、面向含整数-指针转换程序的端到端验证链。
Although there have been many approaches for developing formal memory models that support integerpointer casts, previous approaches share the drawback that they are not designed for end-to-end verification ,failing to support some important source-level coding patterns, justify some backend optimizations, or lack a source-level logic for program verification. This paper presents Archmage, a framework for integer-pointer casting designed for end-to-end verification,supporting a wide range of source-level coding patterns, backend optimizations, and a formal notion of out-ofmemory. To facilitate end-to-end verification via Archmage, we also present two systems based on Archmage: CompCertCast, an extension of CompCert with Archmage to bring a full verified compilation chain to integer-pointer casting programs, and Archmage logic, a source-level logic for reasoning about integerpointer casts. We design CompCertCast such that the overhead from formally supporting integer-pointer casts is mitigated, and illustrate the effectiveness of Archmage logic by verifying an xor-based linked-list implementation, Together, our paper presents the first practical end-to-end verification chain for programs containing integer-pointer casts.
@article{KimCLKYSH25,
title = {Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting},
author = {Yonghyun Kim and Minki Cho and Jaehyung Lee and Jinwoo Kim and Taeyoung Yoon and Youngju Song and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704881}
}