39 citations · 146 across the 23 of their papers we have counts for
26 papers
A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism
Shawn Ong, Dexter Kozen
We give a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism introduced in Ong, Ma, and Kozen (2025).
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…
Probability and Angelic Nondeterminism with Multiset Semantics
Shawn Ong, Stephanie Ma, Dexter Kozen
We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over m…
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva +1
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but the…
A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
Jan Rooduijn, Dexter Kozen, Alexandra Silva
Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following e…
Joint Distributions in Probabilistic Semantics
Dexter Kozen, Alexandra Silva, Erik Voogd
Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability di…