一句话：提出按空间与时间两轴分解翻译验证问题，利用编译器信息提升可扩展性，验证更多翻译并加速。
翻译验证判断程序变换前后 P 与 P′ 语义是否一致，是编译器测试与形式验证之间的折中，但性能瓶颈限制其采用。本文提出按空间和时间两轴分解翻译验证问题：空间轴上利用编译器信息提取子程序，使子程序等价可蕴含整体变换等价；时间轴上利用编译器信息动态分组待验证的变换 pass。评估表明，该方法能验证现有方法失败的 10% 翻译，并将验证速度最多提升 2.4 倍。
Translation validation is a critical tool in program analysis: when a program P is transformed into a new program P ′, translation validation asks whether P and P ′ have the same semantics. It serves as a middle ground between compiler testing and formal verification, capable of proving that a particular run of a compiler produced correct results. However, one bottleneck holds back wider adoption of translation validation: performance. State-of-the-art tools frequently time out or require extensive manual engineering to adapt to specific use cases. In this paper, we propose a new approach to improving the scalability of translation validation by decomposing the problem along two axes. Our primary contribution is a method for harnessing compiler information to extract subprograms whose equivalence result implies equivalence of the overall transformation (the spatial axis). We augment this method by utilizing compiler information to dynamically group transformation passes for validation (the temporal axis). Our evaluation demonstrates that this approach validates 10% of translations that existing approaches fail to validate, and speeds up validation by up to 2.4×.
@article{paperbot12107,
title = {Spatial and Temporal Decomposition for Faster Translation Validation},
author = {Benjamin Mikek and Chathur Bommineni and Qirun Zhang and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839512}
}