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).



Kirigami, The Verifiable Art of Network Cutting1


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



1 See here for an explanation of the title.