Verification and Synthesis

Network controllers are complex software systems that must simultaneously implement a wide range of policies and services on top of a highly asynchronous environment (the network). As any complex software systems, network controllers are likely to be plagued by bugs that must be discovered and fixed. While discovering these bugs is often hard, fixing them is even harder. As network controllers are critical entity, they cannot simply be “rebooted”, they must run at all time to ensure smooth and continuous network operations. As such, network controllers need also to be upgraded on-the-fly.

Our group is involved in verifying that network controllers are correct through static and dynamic analysis. We are also studying how we can make network controller “hot-swappable”, enabling controllers to be upgraded at runtime without creating any disruption.

Active Members

Tibor Schneider
PhD student
Roland Schmid
PhD student
Yu Chen
PhD student


Taming the transient while reconfiguring BGP

The three tales of (correct) network operations

Snowcap: Synthesizing Network-Wide Configuration Updates

Blog Posts

Selected Publications

Luca Beurer-Kellner, Martin Vechev, Laurent Vanbever, and Petar Veličković
NeurIPS '22
Rüdiger Birkner, Tobias Brodmann, Petar Tsankov, Laurent Vanbever, and Martin Vechev
NSDI '21
Samuel Steffen, Timon Gehr, Petar Tsankov, Laurent Vanbever, and Martin Vechev

Available Student Theses

Running Student Theses