超越大规模KAT：针对GKAT变种的高效决策过程
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
AI总结：
本文提出了一种高效的决策过程，用于GKAT变种的轨迹等价性，并通过实验展示了其在控制流转换中的实用性及性能优势。
摘要：
本文提出了几种高效的决策过程，用于GKAT自动机的轨迹等价性，这些过程利用了通过SAT求解器的即时符号技术。为了展示我们算法的适用性，我们为基于GKAT设计的实用系统CF-GKAT设计了符号导数，该系统用于验证控制流转换。我们用Rust实现了这些算法，并在随机生成的基准和真实世界控制流转换上进行了评估。确实，我们观察到在KAT和CF-GKAT上，与现有实现相比，性能提升了数量级。值得注意的是，我们的实验还揭示了行业标准反编译器Ghidra中的一个bug，突显了这些系统在实际中的可行性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
