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
Talks
Taming the transient while reconfiguring BGP
The three tales of (correct) network operations
Snowcap: Synthesizing Network-Wide Configuration Updates
Blog Posts
Taming the transient while reconfiguring BGP
October 24, 2023
NetDice verifies your SLAs using probabilistic analysis
October 15, 2020
You can’t verify what you can’t specify
May 11, 2020
Selected Publications
Available Student Theses
Supervisors: Tibor Schneider and Laurent Vanbever
Running Student Theses
Student: Jonathan Rappl
Supervisors: Tibor Schneider, Yu Chen, Alexander Dietmüller, and Laurent Vanbever