Showing cs.LOShow all
3 papers · 1 filter
cs.LO2024
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…
cs.LO2024
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…
cs.LO2024
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…