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中的一个错误，这凸显了这些系统的实际可行性。