CF-GKAT: Efficient Validation of Control-Flow Transformations

This video presents research on Control-Flow GKAT (CF-GKAT), a framework that extends Guarded Kleene Algebra with Tests to overcome its limitations in reasoning about program equivalence. Learn how CF-GKAT enables sound and complete verification of trace equivalence for programs with non-local control flow (such as goto, break, and return) and hardcoded values, while maintaining nearly-linear efficiency. The presentation demonstrates practical applications in validating complex program transformations, including Erosa and Hendren's goto-elimination procedure and outputs from the Ghidra decompiler. Discover how this advancement expands the application of Kleene Algebra to broader challenges in decompilation and control-flow transformation verification. The 21-minute talk was delivered at the POPL 2025 conference by researchers from University College London, Leiden University, Virginia Tech, and the Open University of the Netherlands, with supplementary materials and artifacts available for further exploration.