CF-GKAT: Efficient Validation of Control-Flow Transformations

on YouTube ↗21m

" summary

Extends GKAT to handle hardcoded indicator variables and non‑local control flow (goto, break, return) and proves sound, complete trace‑equivalence by introducing continuation semantics and a CFG‑GKAT automaton model. Uses a Thompson construction to compile programs to automata, lowers to GKAT automata, and reduces equivalence to bisimulation, preserving nearly‑linear performance. Prototype validates real decompiler transformations (including Ghidra and goto‑elimination) and checks a nasty function in about 0.5s.

AI-written summary · about

" chapters (14)

1. 0:00CF-GKAT introduction
2. 1:46Control flow restructuring
3. 3:36Current restructuring tech
4. 5:44Trace equivalence and GKAT
5. 7:49Indicator variables challenges
6. 9:52Continuation semantics
7. 11:39Operational semantics with CFG-cat
8. 13:45Thompson’s construction proofs
9. 15:51Trace equivalence decision
10. 16:58Implementation results
11. 17:41Future work and optimizations
12. 18:42Q&A on probabilistic systems
13. 19:46Q&A on non-local control flow
14. 20:30Closing remarks