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 of an automatic verification tool. Domain-specific
optimizations and a parallelizing backend enable
McNetKAT to analyze networks with thousands of nodes,
automatically reasoning about general properties such as probabilistic
program equivalence and refinement, as well as networking properties
such as resilience to failures. We evaluate McNetKAT's scalability
using real-world topologies, compare its performance against
state-of-the-art tools, and develop an extended case study on a
recently proposed data center network design.
Mon 24 Jun Times are displayed in time zone: Tijuana, Baja California change
14:00 - 15:30: Probabilistic ProgrammingPLDI Research Papers at 224AB Chair(s): Martin HirzelIBM Research | |||
14:00 - 14:20 Talk | Scalable Verification of Probabilistic Networks PLDI Research Papers Steffen SmolkaCornell University, Praveen KumarCornell University, David M. KahnCarnegie Mellon University, USA, Nate FosterCornell University, Justin HsuUniversity of Wisconsin-Madison, USA, Dexter KozenCornell University, Alexandra SilvaUniversity College London DOI Pre-print Media Attached | ||
14:20 - 14:40 Talk | Cost Analysis of Nondeterministic Probabilistic Programs PLDI Research Papers Peixin WangShanghai Jiao Tong University, Hongfei FuIST Austria, Amir Kafshdar GoharshadyIST Austria, Krishnendu ChatterjeeIST Austria, Xudong QinEast China Normal University, China, Wenjun ShiEast China Normal University, China Media Attached | ||
14:40 - 15:00 Talk | Gen: A General-Purpose Probabilistic Programming System with Programmable Inference PLDI Research Papers Marco Cusumano-TownerMIT-CSAIL, Feras SaadMassachusetts Institute of Technology, Alexander K. LewMassachusetts Institute of Technology, USA, Vikash MansinghkaMIT Media Attached | ||
15:00 - 15:20 Talk | Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs PLDI Research Papers Media Attached |