State of the art languages and tools for network programming and verification are fundamtentally limited, because they are based on deterministic network models. But real-world networks have many important features that are inherently non-deterministic:
Probabilistic NetKAT is a language and framework that allows modeling, programming, and reasoning about networks with such probabilistic fatures. It seeks to answer quantitative questions such as:
Cornell
UCLDavid M. Kahn. Undecidable Problems for Probabilistic Network Programming. In International Symposium on Mathematical Foundations of Computer Science (MFCS), Aalborg, Denmark, July 2017. [ full version ]
Robert Furber, Dexter Kozen, Kim Larsen, Radu Mardare, and Prakash Panangaden. Unrestricted Stone duality for Markov processes. In ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), June 2017. [ conference version ]
Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. In Can Başkent, Lawrence S. Moss, and Ramaswamy Ramanujam, editors, Rohit Parikh on Logic, Language and Society. March 2017. [ conference version ]
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, January 2017. [ conference version | full version | slides ]
Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In European Symposium on Programming (ESOP), Eindhoven, Netherlands, April 2016. [ conference version ]
Probabilistic NetKAT is supported by ERC Starting Grant 679127; the National Security Agency; the National Science Foundation under grants CNS-1111698, CNS- 1413972, CCF-1422046, CCF-1253165, and CCF-1535952; the Office of Naval Research under grant N00014-15-1-2177; the Dutch Research Foundation (NWO) under project numbers 639.021.334 and 612.001.113; and gifts from Cisco, Facebook, Google, and Fujitsu.
