We tackle the problem of deciding whether two probabilistic programs are equivalent in the context of Probabilistic NetKAT, a formal language for reasoning about the behavior of packet-switched networks.
The main challenge lies in reasoning about iteration, which we address by a reduction to finite-state absorbing Markov chains. Building on this approach, we develop an effective decision procedure based on stochastic matrices. Through an extended case study with a real-world data center network, we show how to use these techniques to
automatically verify various properties of interests, including resilience in the presence of failures. This is joint work with Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, and Dexter Kozen.