一句话：提出 CF-GKAT，扩展 GKAT 以支持非局部控制流和硬编码值，高效可靠完备地验证控制流变换的迹等价。
GKAT（带测试的守卫 Kleene 代数）为简单命令式程序的迹等价提供了可靠且完备的推理框架，但存在两个局限：它完全忽略原语的语义，且不支持 goto、break、return 等非局部控制流。为克服这些限制，本文引入 Control-Flow GKAT（CF-GKAT），该体系能够推理包含非局部控制流及硬编码值的程序。CF-GKAT 可对更大类程序进行可靠且完备的迹等价验证，同时保持 GKAT 近乎线性的效率。这使得它适用于验证控制流操作过程，如反编译和 goto 消除。作者通过验证多个高度非平凡的程序变换（包括 Erosa 和 Hendren 的 goto 消除过程以及 Ghidra 反编译器的输出）展示了 CF-GKAT 的能力，为 Kleene 代数在反编译与控制流变换领域开辟了更广泛的应用。
Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break , and return . To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT) , a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT’s abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren’s goto -elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ZhangKNN25,
title = {CF-GKAT: Efficient Validation of Control-Flow Transformations},
author = {Cheng Zhang and Tobias Kappé and David E. Narváez and Nico Naus},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704857}
}