Mon 24 Jun 2019 14:00 - 14:20 at 224AB - Probabilistic Programming Chair(s): Martin Hirzel

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

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Probabilistic ProgrammingPLDI Research Papers at 224AB
Chair(s): Martin Hirzel IBM Research
14:00
20m
Talk
Scalable Verification of Probabilistic Networks
PLDI Research Papers
Steffen Smolka Cornell University, Praveen Kumar Cornell University, David M. Kahn Carnegie Mellon University, USA, Nate Foster Cornell University, Justin Hsu University of Wisconsin-Madison, USA, Dexter Kozen Cornell University, Alexandra Silva University College London
DOI Pre-print Media Attached
14:20
20m
Talk
Cost Analysis of Nondeterministic Probabilistic Programs
PLDI Research Papers
Peixin Wang Shanghai Jiao Tong University, Hongfei Fu IST Austria, Amir Kafshdar Goharshady IST Austria, Krishnendu Chatterjee IST Austria, Xudong Qin East China Normal University, China, Wenjun Shi East China Normal University, China
Media Attached
14:40
20m
Talk
Gen: A General-Purpose Probabilistic Programming System with Programmable Inference
PLDI Research Papers
Marco Cusumano-Towner MIT-CSAIL, Feras A. Saad Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, USA, Vikash K. Mansinghka MIT
Media Attached
15:00
20m
Talk
Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs
PLDI Research Papers
Jieyuan Zhang UNSW, Australia, Jingling Xue UNSW Sydney
Media Attached