NDD: A Decision Diagram for Network Verification

on YouTube ↗15m

" summary

Introduces Network Decision Diagram (NDD), a two-layer structure that groups header bits into fields and builds per-field BDDs while assembling them with nodes whose edges are labeled with BDDs, so each edge encodes a whole field value rather than single bits. Re-implements five BDD-based verifiers (including Batfish and control-plane tools) with minor code changes and observes a 100× memory reduction and 100× speedup, plus fewer equivalence classes and shallower recursion.

AI-written summary · about

" chapters (6)

1. 0:00Introduction and background
2. 1:57BDD overview and limitations
3. 3:31Analyzing BDD limitations
4. 7:19Introducing NDD
5. 11:37NDD evaluation and results
6. 14:41Conclusion and Q&A

" related talks

• 17mDifferential Network AnalysisXu Liu, Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Hao Li · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 18mReachability Analysis of the Domain Name SystemDavid Basin, Dhruv Nevatia, Si Liu · POPL 2025
• 25mDataplane equivalence and its applicationsDragos Dumitrescu, Costin Raiciu, Radu Stoenescu, Matei Popovici, Lorina Negreanu · NSDI 2019
• 25mEnsuring Connectivity via Data Plane MechanismsScott Shenker, Brighten Godfrey, Aurojit Panda, Ankit Singla, Michael Schapira, Junda Liu · NSDI 2013
• 12mMetha: Network Verifiers Need To Be Correct Too!Martin Vechev, Laurent Vanbever, Rüdiger Birkner, Tobias Brodmann, Petar Tsankov · NSDI ’21
• 18mLiveness Verification of Stateful Network FunctionsAditya Akella, Soudeh Ghorbani, Anubhavnidhi Abhashkumar, Farnaz Yousefi, Kausik Subramanian, Kartik Hans · NSDI 2020
• 14mEPVerifier: Accelerating Update Storms Verification with Edge-PredicateChenyang Zhao, Haifeng Sun, Yuebin Guo, Jingyu Wang, Qi Qi, Zirui Zhuang, Lingqi Guo, Yuming Xie, Jianxin Liao · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)
• 25mNetwork Change Validation with Relational NetKATHan Xu, Zachary Kincaid, David Walker, Ratul Mahajan · POPL 2026