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.

翻译：带测试的守卫克林代数（GKAT）为推理简单命令式程序间的迹等价提供了一个可靠且完备的框架。然而，该框架仍存在若干显著局限性。首先，为保持等价性可判定，GKAT完全忽略原语的具体语义。其次，GKAT排除了非局部控制流，例如goto、break和return。为克服这些局限，我们提出了控制流GKAT（CF-GKAT），该系统能够推理包含非局部控制流及硬编码值的程序。CF-GKAT能够可靠且完备地验证更广泛程序类的迹等价性，同时保持GKAT近乎线性的效率。这使得CF-GKAT适用于验证控制流操纵过程，如反编译和goto消除。为展示CF-GKAT的能力，我们验证了若干高度非平凡程序变换的输出，例如Erosa和Hendren的goto消除过程以及Ghidra反编译器的输出。CF-GKAT将克林代数的应用拓展至更广泛的挑战领域，并为反编译与控制流变换领域提供了重要的验证工具。