3 papers
cs.PL2025
StacKAT: Infinite State Network Verification
Jules Jacobs, Nate Foster, Tobias Kappé +4
We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and - most importantly - access to a stack with accompanying push and p…
cs.PL2025
Algebras for Deterministic Computation Are Inherently Incomplete
Balder ten Cate, Tobias Kappé
Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic pr…
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…