Network Verification and BDDs (Zhenrong Gu, XJTU)

Network outages caused by configuration errors and data-plane bugs have become routine headlines, and formal verification is the natural response. Tools such as APKeep and Symbolic Router Execution (SRE) model a network as a graph of standardized packet (or route) filters and transformers, and symbolically simulate packet forwarding, reducing an intractable header space to a small number of equivalence classes represented as BDDs. With the rapid expansion of data centers, this approach is facing scalability issues. One observation makes such representations far cheaper: the variables in a network verification problem are organized into fields, and the logic over each field is highly repetitive and reusable across devices. Network Decision Diagrams (NSDI '25) exploit this by branching one field at a time and representing each edge as a shareable BDD, yielding large speedups and memory savings for APKeep and improved scalability for SRE. I will then discuss two limits of NDDs: quantitative properties requiring multi-terminal representations, and the difficulty of choosing a field granularity for link status. Both may be addressed by Generalized CFLOBDDs, introduced by Meghana Sistla, which use a custom grammar to describe variable organization and permit a loose recursive hierarchy with external decision diagrams at the leaves. Building on that idea, I have been formalizing the structure: a Rust implementation, a canonicity proof, structural optimizations, and an evaluation on network verification and quantum simulation. I will present the canonicity argument and these early results, and close with some open questions about the future of NDDs and CFLOBDDs.