# Scalable Verification of Probabilistic Networks

## TL;DR

McNetKAT is a scalable verification tool for probabilistic network programs that uses Markov chain semantics to analyze large networks efficiently, enabling automatic reasoning about network properties and failures.

## Contribution

Introduces McNetKAT, a novel scalable verification framework for probabilistic networks based on Markov chain semantics, capable of analyzing networks with thousands of nodes.

## Key findings

- Successfully verified real-world network topologies.
- Outperformed existing verification tools in scalability.
- Validated effectiveness on a data center network case study.

## Abstract

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.