Han Xu will present his General Exam " Relational Netkat" on May 2, 2025 at 10am in CS 402 and Zoom. Committee: David Walker (adviser), Zachary Kincaid, Maria Apostolaki Zoom link: [ https://princeton.zoom.us/j/8011315368 | https://princeton.zoom.us/j/8011315368 ] Abstract: Modern networks are complex, dynamic, and large-scale, making network verification a critical challenge. Relational NetKAT extends traditional NetKAT by providing an expressive and efficient framework for reasoning about network behavior under path changes, forwarding table modifications, and network topology updates. It enables all-path verification, ensuring that network-wide invariants hold across diverse changes such as load balancing and routing updates. Compared to sample-based verification of Rela, which fails to cover all possible paths, Relational NetKAT provides a mathematically sound and scalable approach to checking network correctness. Reading List: Textbook: * Types and programming languages. MIT press, 2002. * Handbook of Model Checking Ch 7.8. Paper: Netkat, Kleene algebra and automata theory * Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David Walker, and Ennan Zhai. 2024. Relational Network Verification. * Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: semantic foundations for networks. * Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. * Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. BDD and Model Checking * Bryant Randy, 1992. Symbolic Boolean manipulation with ordered binary-decision diagrams * Kathi Fisler and Moshe Y. Vardi. 2002. Bisimulation Minimization and Symbolic Model Checking. Network Verification * H. Yang and S. S. Lam, "Real-time verification of network properties using Atomic Predicates," 2013 * Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header space analysis: static checking for networks. * Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2012. Veriflow: verifying network-wide invariants in real time.