This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.

翻译：本文提出了几种针对GKAT自动机迹等价的高效决策过程，这些过程通过SAT求解器利用即时符号化技术实现。为展示我们算法的适用性，我们为CF-GKAT设计了符号导数——这是一个基于GKAT设计的实用系统，用于验证控制流转换。我们在Rust语言中实现了这些算法，并在随机生成的基准测试和真实世界控制流转换上进行了评估。实验结果表明，相较于现有的KAT和CF-GKAT实现，我们的方法在性能上实现了数量级的提升。值得注意的是，实验还揭示了行业标准反编译器Ghidra中存在的一个错误，这进一步凸显了这些系统的实际应用价值。