General Exam

I took my general exam on May 18th, 2020 at 11:00 EST. Below are listed my committee members, my abstract and my reading list. See these links for the Keynote slides and the PDF (zipped) (note: these are large files).

Committee

• Aarti Gupta (advisor)
• David Walker
• Zak Kincaid

Title

Kirigami, The Verifiable Art of Network Cutting¹

Abstract

Existing network verification techniques do not scale to large, real-world networks. We investigate partitioning a network into multiple components to reduce the burden of verification of the stable routing problem (SRP), by cutting the network into multiple composable partitions, calculating separate solutions and then verifying them individually to obtain a proof for the original SRP instance.
We propose a generalized model for "open SRPs", which are a superset of regular (closed) SRPs, which allow us to define compositions and partitions of open SRPs in terms of interfaces. We show that given a correct interface, we can check SRP properties for partitioned SRPs and reconnect the partitions without invalidating the property. We provide a concrete semantics for open SRPs and their compositions, and we show that the SRP interfaces form a complete lattice, enabling us to apply abstract interpretation techniques to approximate correct interfaces. We connect these semantics to rely-guarantee reasoning and show how our interfaces function as invariants over the cross-partition edges of the SRP.
We provide some examples of these processes from nv, a programming language for simulating and verifying synthetic networks. We develop an extension, Kirigami, which allows an nv programmer to write and check these interfaces.

Reading List

Papers/Chapters

• Fogel, Ari, et al. "A general approach to network configuration analysis." 12th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 15). 2015.
• Griffin, Timothy G., F. Bruce Shepherd, and Gordon Wilfong. "The stable paths problem and interdomain routing." IEEE/ACM Transactions On Networking 10.2 (2002): 232-243.
• Jayaraman, Karthick, et al. "Validating datacenters at scale." Proceedings of the ACM Special Interest Group on Data Communication. 2019. 200-213.
• Barrett, Clark, et al. "Satisfiability Modulo Theories, Handbook of Satisfiability, chapter 12." (2008): 737-797.
• Giannakopoulou, Dimitra, Kedar S. Namjoshi, and Corina S. Păsăreanu. "Compositional reasoning." Handbook of Model Checking. Springer, Cham, 2018. 345-383.
• Jhala, Ranjit, and Rupak Majumdar. "Software model checking." ACM Computing Surveys (CSUR) 41.4 (2009): 1-54.
• Torlak, Emina, and Rastislav Bodik. "A lightweight symbolic virtual machine for solver-aided host languages." ACM SIGPLAN Notices 49.6 (2014): 530-541.
• Milner, Robin, and Mads Tofte. "Co-induction in relational semantics." Theoretical computer science 87.1 (1991): 209-220.
• Xu, Qiwen, Willem-Paul de Roever, and Jifeng He. "The rely-guarantee method for verifying shared variable concurrent programs." Formal Aspects of Computing 9.2 (1997): 149-174.

Textbooks

• Pierce, Benjamin C., and C. Benjamin. Types and programming languages. MIT press, 2002.
• Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007.

¹ See here for an explanation of the title.