Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time

Steffen Smolka, Nate Foster, Justin Hsu +3

Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($\ast$) operations from KAT to pre…