Scalable Verification of Probabilistic Networks
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 190-203, 2019.
This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction o...More
PPT (Upload PPT)