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:
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.