a probabilistic language for networks

Learn More »

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:

  • Efficient routing protocols distribute flows across multiple paths for better performance.
  • Link failures occur randomly in a network, and
  • Fault-tolerance mechanisms resort to backup paths when links fail.

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:

  • What is the expected congestion of a link, given some model of the network demand?
  • What is the probability of packet delivery, given some failure model of the links?
  • What is the expected latency, given some randomized routing algorithm?

Cornell Cornell



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.

  • ERC
  • NSA
  • NSF
  • ONR
  • NWO
  • Facebook
  • Google
  • Fujitsu