一句话：提出三维精化代数及其组合语义框架，并在 Coq 中统一组合式验证与认证编译。
形式验证是构建可靠系统的黄金标准，但大规模异构系统的验证仍超出当前技术能力，亟需能兼容并衔接多种程序验证与认证编译技术的组合式方法。现有组合语义工具常依赖简单且专用的操作模型，难以互操作。本文提出一个组合式语义框架，其核心是三维精化代数：精化可跨程序模块、抽象层次与系统状态组件进行组合。该框架在 Coq 证明助手中机械化，作者通过多个用例展示其能容纳广泛的验证技术，并为组合验证与认证编译提供统一语义基础。
Formal verification is a gold standard for building reliable computer systems. Certified systems in particular come with a formal specification, and a proof of correctness which can easily be checked by a third party. Unfortunately, verifying large-scale, heterogeneous systems remains out of reach of current techniques. Addressing this challenge will require the use of compositional methods capable of accommodating and interfacing a range of program verification and certified compilation techniques. In principle, compositional semantics could play a role in enabling this kind of flexibility, but in practice existing tools tend to rely on simple and specialized operational models which are difficult to interface with one another. To tackle this issue, we present a compositional semantics framework which can accommodate a broad range of verification techniques. Its core is a three-dimensional algebra of refinement which operates across program modules, levels of abstraction, and components of the system’s state. Our framework is mechanized in the Coq proof assistant and we showcase its capabilities with multiple use cases.
@article{ZhangKSW25,
title = {Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra},
author = {Yu Zhang and Jérémie Koenig and Zhong Shao and Yuting Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704900}
}