3 papers
cs.PL2026
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji +3
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 a…
cs.PL2025
CF-GKAT: Efficient Validation of Control-Flow Transformations
Cheng Zhang, Tobias Kappé, David E. Narváez +1
Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still seve…
math.LO2024
Kleene algebra with commutativity conditions is undecidable
Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in…