Dexin Zhang will present his General Exam "Modular Verification and Repair for Networks" on Monday, May 5, 2025 at 10am in CS 402. Committee: Aarti Gupta (adviser), David Walker, Mae Milano Abstract: Large industrial networks connect millions of servers with hundreds of thousands of network devices. To improve these systems’ reliability, researchers have turned to modular verification techniques to break these large networks into smaller pieces to analyze independently. Unfortunately, in doing so, researchers face tradeoffs. More expressive frameworks can verify a wider range of properties, but often place a greater burden on the user to describe network behavior at the interfaces between components. We present CB-graphs, a new framework for modular network control plane verification that navigates these tradeoffs using graph-based abstractions, allowing it to verify a rich set of properties while simplifying the interfaces a user must supply. Users construct CB-graphs that describe which network devices converge before others. Interfaces between nodes in these graphs may contain more or less information, depending on what is convenient and needed to prove the desired properties. We develop a theory of CB-graph-based verification and prove it sound via a formalization in the Lean theorem prover. We exploit our framework to develop a new, scalable method for local repair of network configurations. We implement our verification and repair algorithms in a tool called CB-Ver, and evaluate its performance on a range of benchmarks.