111 citations · 528 across the 50 of their papers we have counts for
5 papers · 2 filters
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
Wojciech Różowski, Tobias Kappé, Dexter Kozen +2
We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branc…
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Noam Zilberstein, Angelina Saliling, Alexandra Silva
Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many pro…
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Noam Zilberstein, Derek Dreyer, Alexandra Silva
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundati…
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Tobias Kappé, Todd Schmid, Alexandra Silva
Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast…
Multisets and Distributions
Dexter Kozen, Alexandra Silva
We give a lightweight alternative construction of Jacobs's distributive law for multisets and distributions that does not involve any combinatorics. We first give a distributive la…