NDD: A Decision Diagram for Network Verification#
NSDI '25 digest Program Adjacent pick 28–30 April 2025
- Authors / tier: Zechun Li, Peng Zhang, Yichi Zhang (Xi'an Jiaotong University); Hongkun Yang (Google). Adjacent. Awarded Outstanding Paper.
- Why: Network verification underpins config-change safety and reachability analysis. BDDs have been the standard data structure for a decade; an Outstanding Paper that improves the substrate is worth tracking even if you consume verification rather than build it.
- What: Network Decision Diagram (NDD), a data structure customized for verification that natively supports equivalence classes and beats BDD on memory and computation.
- How: NDD wraps BDD in another decision-diagram layer — each NDD node represents a header field, and each edge is labeled with a BDD encoding that field's values. Because field-based matching is local, NDD sharply reduces BDD node counts and makes equivalence-class handling transparent to verifiers. Released as a library; existing verifiers (AP Verifier, APT) were ported to it.
- Where applicable: General — a drop-in substrate for BDD-based verification tools.