Campus Event Calendar
Event Entry
What and Who
Probabilistic Program Equivalence for NetKAT
Alexandra Silva
University College, London
SWS Colloquium
SWS, MMCI
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 2 May 2018
10:30
90 Minutes
E1 5
029
Saarbrücken
Abstract
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.
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.
Contact
Claudia Richter
9303 9103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
113
passcode not visible
logged in users only
Claudia Richter, 04/30/2018 10:55 -- Created document.