Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

TL;DR

This work advances decision procedures for GKAT and its CF-GKAT extension by introducing on-the-fly and symbolic techniques that avoid full automaton construction. It couples derivative-based generation with Boolean-formula transitions and SAT/BDD backends to compress state spaces and accelerate trace-equivalence checks, achieving substantial practical speedups over prior methods. The authors provide formal correctness and complexity results, implement a Rust prototype, and demonstrate performance gains on synthetic benchmarks and real-world control-flow transformations, including uncovering a bug in Ghidra. The approach broadens the applicability of GKAT-based verification to large-scale programs and complex CF-GKAT constructs, showing tangible impact for software verification and decompiler analysis.

Abstract

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.

Figures (11)

• Figure 1: Two finite-trace equivalent CF-GKAT programs, where $(q; \texttt{assert}~t_{1} \land \overline{t_{2}})$ encodes the knowledge that the test $t_{1} \land \overline{t_{2}}$ always holds after action $q$.
• Figure 2: A summary of algorithms mentioned in this paper: the original one is marked in red; the on-the-fly is marked in blue; and the symbolic on-the-fly is marked in green.
• Figure 3: The automata generated for programs in \ref{['fig:equiv-cfgkat-prog']} using the algorithm in zhang_CFGKATEfficientValidation_2025. We omit transitions that output rejection. All the dead states of the automata are highlighted in red and equivalent states are marked using the same colors.
• Figure 4: On the left, an erroneous version of the low-level program that is not trace equivalent to \ref{['fig:high-level-equiv-cfgkat-prog']}, where the $t_{1} \lor t_{2}$ in the first if-statement is mistaken as $t_{1}$. On the right, the corresponding automaton (with omitted reject transitions).
• Figure 5: Non-symbolic on-the-fly bisimulation algorithm. The call isDead($s$) first checks whether $s$ is in the set of cached "known-dead states" (knownDead($s$)): if so, returns true, else it runs a DFS to see if the state $s$ can reach any accepting state; if $s$ cannot reach an accepting state, all the reachable states of $s$ are cached as known-dead states. The call union($s, u$) links $s, u$ to the same representative in the union-find object, and rep($s$) returns the representative of $s$ from said union-find object. "iff", "and", "implies" are the respective logical operators on Booleans, and $\&\!\&$ is the logical conjunction.

Theorems & Definitions (13)

• remark thmcounterremark
• remark thmcounterremark
• definition thmcounterdefinition: Trace Semantics smolka_GuardedKleeneAlgebra_2020
• theorem thmcountertheorem: Correctness
• definition thmcounterdefinition: Symbolic GKAT Automata
• definition thmcounterdefinition: Concretization
• remark thmcounterremark: Determinacy
• remark thmcounterremark: Blocked Transition
• theorem thmcountertheorem: Correctness
• remark thmcounterremark: Thompson's Construction v.s. Derivatives