Research

Network Verification & Synthesis Reading List

Download BibTeX >>

Data Plane Verification

  • [HSA] Kazemian, P.; Varghese, G. and McKeown, N. Header Space Analysis: Static Checking for Networks. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2012. [pdf] 
  • [NetPlumber] Kazemian, P.; Chang, M.; Zeng, H.; Varghese, G.; McKeown, N. and Whyte, S. Real Time Network Policy Checking Using Header Space Analysis. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2013. [pdf] 
  • [Anteater] Mai, H.; Khurshid, A.; Agarwal, R.; Caesar, M.; Godfrey, P. B. and King, S. T. Debugging the data plane with Anteater. In SIGCOMM, 2011. [pdf] 
  • [ATPG] Zeng, H.; Kazemian, P.; Varghese, G. and McKeown, N. Automatic Test Packet Generation. In CoNEXT, 2012. [pdf] 
  • [VeriFlow] Khurshid, A.; Zou, X.; Zhou, W.; Caesar, M. and Godfrey, P. B. VeriFlow: Verifying Network-wide Invariants in Real Time. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2013. [pdf] 
  • [NoD] Lopes, N. P.; Bjorner, N.; Godefroid, P.; Jayaraman, K. and Varghese, G. Checking Beliefs in Dynamic Networks. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2015. [pdf] 
  • Plotkin, G. D.; Bjorner, N.; Lopes, N. P.; Rybalchenko, A. and Varghese, G. Scaling network verification using symmetry and surgery. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016. [pdf]  [doi] 
  • [SymNet] Stoenescu, R.; Popovici, M.; Negreanu, L. and Raiciu, C. SymNet: Scalable symbolic execution for modern networks. In SIGCOMM, 2016. [doi] 
  • [Delta-net] Horn, A.; Kheradmand, A. and Prasad, M. R. Delta-net: Real-time Network Verification Using Atoms. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017. [pdf] 
  • [RCDC/SecGuru] Jayaraman, K.; Bjorner, N.; Padhye, J.; Agrawal, A.; Bhargava, A.; Bissonnette, P-A. C.; Foster, S.; Helwer, A.; Kasten, M.; Lee, I.; Namdhari, A.; Niaz, H.; Parkhi, A.; Pinnamraju, H.; Power, A.; Raje, N. M. and Sharma, P. Validating datacenters at scale. In Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM), 2019. [pdf] 
  • [Tiros] Backes, J.; Bayless, S.; Cook, B.; Dodge, C.; Gacek, A.; Hu, A. J.; Kahsai, T.; Kocik, B.; Kotelnikov, E.; Kukovec, J.; McLaughlin, S.; Reed, J.; Rungta, N.; Sizemore, J.; Stalzer, M. A.; Srinivasan, P.; Subotic, P.; Varming, C. and Whaley, B. Reachability Analysis for AWS-Based Networks. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV), 2019. [pdf] 
  • [APKeep] Zhang, P.; Liu, Xu; Yang, H.; Kang, N.; Gu, Z. and Li, H. APKeep: Realtime Verification for Real Networks. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020. [pdf] 
  • Bayless, S.; Backes, J. D.; DaCosta, D.; Jones, B. F.; Launchbury, N.; Trentin, P.; Jewell, K.; Joshi, S.; Zeng, M. Q. and Mathews, N. Debugging Network Reachability with Blocked Paths. In 33rd International Conference on Computer Aided Verification (CAV), 2021. [pdf] 
  • [Katra] Beckett, R. and Gupta, A. Katra: Realtime Verification for Multilayer Networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2022. [pdf] 
  • [Flash] Guo, D.; Chen, S.; Gao, K.; Xiang, Q.; Zhang, Y. and Yang, Y. R. Flash: fast, consistent data plane verification for large-scale network settings. In ACM SIGCOMM Conference, 2022. [pdf]  [doi] 
  • Arashloo, M. T.; Beckett, R. and Agarwal, R. Formal Methods for Network Performance Analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2023. [pdf] 

Network Configuration Verification

  • [rcc] Feamster, N. and Balakrishnan, H. Detecting BGP Configuration Faults with Static Analysis. In Proceedings of the 2nd USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2005. [pdf] 
  • [Minerals] Le, F.; Lee, S.; Wong, T.; Kim, H. S. and Newcomb, D. Detecting network-wide and router-specific misconfigurations through data mining. In IEEE/ACM Transactions on Networking, 17 (1), 2009. [pdf] 
  • [Batfish] Fogel, A.; Fung, S.; Pedrosa, L.; Walraed-Sullivan, M.; Govindan, R.; Mahajan, R. and Millstein, T. A General Approach to Network Configuration Analysis. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2015. [pdf] 
  • [ERA] Fayaz, S. K.; Sharma, T.; Fogel, A.; Mahajan, R.; Millstein, T. D.; Sekar, V. and Varghese, G. Efficient Network Reachability Analysis Using a Succinct Control Plane Representation. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016. [pdf] 
  • [Bagpipe] Weitz, K.; Woos, D.; Torlak, E.; Ernst, M. D.; Krishnamurthy, A. and Tatlock, Z. Scalable verification of border gateway protocol configurations with an SMT solver. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. [pdf]  [doi] 
  • [ARC] Gember-Jacobson, A.; Viswanathan, R.; Akella, A. and Mahajan, R. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM, 2016. [pdf] 
  • [Minesweeper] Beckett, R.; Gupta, A.; Mahajan, R. and Walker, D. A General Approach to Network Configuration Verification. In SIGCOMM, 2017. [pdf] 
  • [P-Rex] Jensen, J. S.; Krogh, T. B.; Madsen, J. S.; Schmid, S.; Srba, J. and Thorgersen, M. T. P-Rex: fast verification of MPLS networks with multiple link failures. In Proceedings of the 14th International Conference on emerging Networking EXperiments and Technologies (CoNEXT 2018), 2018. [pdf] 
  • [Bonsai] Beckett, R.; Gupta, A.; Mahajan, R. and Walker, D. Control PLane Compression. In SIGCOMM, 2018. [pdf] 
  • [Origami] Giannarakis, N.; Beckett, R.; Mahajan, R. and Walker, D. Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement. In International Conference on Computer Aided Verification (CAV), 2019. [pdf] 
  • [FastPlane] Lopes, N. P. and Rybalchenko, A. Fast BGP Simulation of Large Datacenters. In Proceedings of the 20th Interntional Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019. [pdf] 
  • Beckett, R. and Mahajan, R. Putting network verification to good use. In Proceedings of the ACM Workshop on Hot Topics in Networks (HotNets), 2019. [pdf] 
  • [NV] Giannarakis, N.; Loehr, D.; Beckett, R. and Walker, D. NV: an intermediate language for verification of network control planes. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), 2020. [pdf] 
  • [ShapeShifter] Beckett, R.; Gupta, A.; Mahajan, R. and Walker, D. Abstract interpretation of distributed network control planes. In Proc. ACM Program. Lang., 4 (POPL), 2020. [pdf] 
  • [Plankton] Prabhu, S.; Chou, K-Y.; Kheradmand, A.; Godfrey, B. and Caesar, M. Plankton: Scalable network configuration verification through model checking. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020. [pdf] 
  • [Tiramisu] Abhashkumar, A.; Gember-Jacobson, A. and Akella, A. Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020. [pdf] 
  • [SelfStarter] Kakarla, S. K. R.; Tang, A.; Beckett, R.; Jayaraman, K.; Millstein, T.; Tamir, Y. and Varghese, G. Finding Network Misconfigurations by Automatic Template Inference. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020. [pdf] 
  • [Hoyan] Ye, F.; Yu, Da; Zhai, E.; Liu, H. H.; Tian, B.; Ye, Q.; Wang, C.; Wu, X.; Guo, T.; Jin, C.; She, D.; Ma, Q.; Cheng, B.; Xu, H.; Zhang, M.; Wang, Z. and Fonseca, R. Accuracy, Scalability, Coverage: A Practical Configuration Verifier on a Global WAN. In SIGCOMM, 2020.
  • [NetDice] Steffen, S.; Gehr, T.; Tsankov, P.; Vanbever, L. and Vechev, M. T. Probabilistic Verification of Network Configurations. In SIGCOMM, 2020. [pdf] 
  • [RealConfig] Zhang, P.; Huang, Y.; Gember-Jacobson, A.; Shi, W.; Liu, Xu; Yang, H. and Zuo, Z. Incremental Network Configuration Verification. In HotNets, 2020. [pdf] 
  • [Campion] Tang, A.; Kakarla, S. K. R.; Beckett, R.; Zhai, E.; Brown, M.; Millstein, T. D.; Tamir, Y. and Varghese, G. Campion: debugging router configuration differences. In ACM SIGCOMM 2021 Conference, 2021. [pdf] 
  • [DNA] Zhang, P.; Gember-Jacobson, A.; Zuo, Y.; Huang, Y.; Liu, Xu and Li, H. Differential Network Analysis. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2022. [pdf] 
  • [SRE] Zhang, P.; Wang, D. and Gember-Jacobson, A. Symbolic router execution. In ACM SIGCOMM Conference, 2022. [pdf]  [doi] 
  • [NetCov] Xu, X.; Deng, W.; Beckett, R.; Mahajan, R. and Walker, D. Test Coverage for Network Configurations. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2023. [pdf] 

Data Plane Synthesis

  • [Genesis] Subramanian, K.; D'Antoni, L. and Akella, A. Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks. In SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017. [pdf]  [doi] 

Network Configuration Synthesis/Repair

  • [Propane] Beckett, R.; Mahajan, R.; Millstein, T.; Padhye, J. and Walker, D. Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations. In SIGCOMM, 2016. [pdf] 
  • [Propane/AT] Beckett, R.; Mahajan, R.; Millstein, T. D.; Padhye, J. and Walker, D. Network configuration synthesis with abstract topologies. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2017. [pdf] 
  • [SyNET] El-Hassany, A.; Tsankov, P.; Vanbever, L. and Vechev, M. T. Network-Wide Configuration Synthesis. In International Conference on Computer Aided Verification (CAV), 2017. [pdf] 
  • [CPR] Gember-Jacobson, A.; Akella, A.; Mahajan, R. and Liu, H. Automatically Repairing Network Control Planes Using an Abstract Representation. In ACM Symposium on Operating Systems Principles (SOSP), 2017. [pdf] 
  • [NetComplete] El-Hassany, A.; Tsankov, P.; Vanbever, L. and Vechev, M. T. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2018. [pdf] 
  • [Zeppelin] Subramanian, K.; D'Antoni, L. and Akella, A. Synthesis of Fault-Tolerant Distributed Router Configurations. In POMACS, 2 (1): 22:1-22:26, 2018. [pdf] 
  • [Jinjing] Tian, B.; Zhang, X.; Zhai, E.; Liu, H. H.; Ye, Q.; Wang, C.; Wu, X.; Ji, Z.; Sang, Y.; Zhang, M.; Yu, Da; Tian, C.; Zheng, H. and Zhao, B. Y. Safely and automatically updating in-network ACL configurations with intent language. In Proceedings of the ACM Special Interest Group on Data Communication (SIGCOMM), 2019. [pdf] 
  • [Snowcap] Schneider, T.; Birkner, R. and Vanbever, L. Snowcap: synthesizing network-wide configuration updates. In ACM SIGCOMM 2021 Conference, 2021. [pdf] 
  • [Aura] Ramanathan, S.; Zhang, Y.; Gawish, M.; Mundada, Y.; Wang, Z.; Yun, S.; Lippert, E.; Taha, W.; Yu, M. and Mirkovic, J. Practical Intent-driven Routing Configuration Synthesis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2023. [pdf] 

Data Plane Repair

  • Hojjat, H.; Rümmer, P.; McClurg, J.; Cern'y, P. and Foster, N. Optimizing horn solvers for network repair. In Formal Methods in Computer-Aided Design (FMCAD), 2016. [pdf] 
  • [NEAt] Zhou, W.; Croft, J.; Liu, B. and Caesar, M. NEAt: Network Error Auto-Correct. In Symposium on SDN Research (SOSR), 2017. [pdf] 

Programmable Control Plane Repair

  • Wu, Y.; Chen, A.; Haeberlen, A.; Zhou, W. and Loo, B. T. Automated Network Repair with Meta Provenance. In ACM Workshop on Hot Topics in Networks (HotNets), 2015. [pdf]  [doi] 

Intent Inference

  • Benson, T.; Akella, A. and Maltz, D. A. Mining policies from enterprise network configuration. In ACM SIGCOMM Internet Measurement Conference (IMC), 2009. [pdf] 
  • [Config2Spec] Birkner, R.; Drachsler-Cohen, D.; Vanbever, L. and Vechev, M. T. Config2Spec: Mining Network Specifications from Network Configurations. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020. [pdf] 
  • [Anime] Kheradmand, A. Automatic Inference of High-Level Network Intents by Mining Forwarding Patterns. In Symposium on SDN Research (SOSR), 2020. [pdf] 

Network Configuration

  • Maltz, D. A.; Xie, G. G.; Zhan, J.; Zhang, H.; Hjálmt'ysson, G. and Greenberg, A. G. Routing design in operational networks: a look from the inside. In SIGCOMM, 2004. [pdf]  [doi] 
  • Benson, T.; Akella, A. and Maltz, D. Unraveling the Complexity of Network Management. In Symposium on Networked Systems Design and Implementation (NSDI), 2009. [pdf] 
  • Benson, T.; Akella, A. and Shaikh, A. Demystifying configuration challenges and trade-offs in network-based ISP services. In SIGCOMM, 2011. [pdf]  [doi] 
  • Kim, H.; Benson, T.; Akella, A. and Feamster, N. The evolution of network configuration: a tale of two campuses. In Proceedings of the 11th ACM SIGCOMM Internet Measurement Conference (IMC), 2011. [pdf] 
  • [MPA] Gember-Jacobson, A.; Wu, W.; Li, X.; Akella, A. and Mahajan, R. Management Plane Analytics. In Proceedings of the 2015 ACM Internet Measurement Conference (IMC), 2015. [pdf]  [doi] 

Network Failures

  • Turner, D.; Levchenko, K.; Snoeren, A. C. and Savage, S. California fault lines: understanding the causes and impact of network failures. In SIGCOMM, 2010. [pdf]  [doi] 
  • Gill, P.; Jain, N. and Nagappan, N. Understanding network failures in data centers: measurement, analysis, and implications. In SIGCOMM, 2011. [pdf]  [doi] 

Miscellaneous

  • [Cocoon] Ryzhyk, L.; Bjorner, N.; Canini, M.; Jeannin, J-B.; Schlesinger, C.; Terry, D. B. and Varghese, G. Correct by Construction Networks Using Stepwise Refinement. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017. [pdf]