Merge branch 'NetworkVerification-master'

Author: ratulm

_config.yml

@@ -50,6 +50,36 @@ authors:
       avatar:         /assets/images/george-varghese.jpg
       bio:            "George Varghese is a Chancellor's Professor of Computer Science at UCLA. He received his Ph.D. in 1992 from MIT after working at DEC designing DECNET protocols and products, including the bridge architecture and Gigaswitch. From 1993-1999, he was a professor at Washington University, and at UCSD from 1999 to 2013. He was the Distinguished Visitor in the computer science department at Stanford University from 2010-2011. From 2012-2016, he was a Principal Researcher and Partner at Microsoft Research working on network verification."
 
+    david:
+      name:           David Walker
+      site:           https://www.cs.princeton.edu/~dpw/
+      avatar:         /assets/images/david-walker.png
+      bio:            "David Walker is a Professor of Computer Science at Princeton University. He received his doctoral and master’s degrees in computer science from Cornell, and his bachelor’s from Queen’s University in Kingston, Ontario.  During sabbaticals from Princeton, he has served as a visiting researcher at Microsoft Research in Redmond (2008) and in Cambridge (2009), and as Associate Visiting Faculty at the University of Pennsylvania (2015-2016)."
+
+    gupta:
+      name:           Aarti Gupta
+      site:           https://www.cs.princeton.edu/~aartig/
+      avatar:         /assets/images/aarti-gupta.jpg
+      bio:            "Aarti Gupta is a Professor of Computer Science at Princeton University. Before joining the department, she worked at NEC Labs America where she led a team in investigating new techniques for formal verification of software and hardware systems, contributing both to their foundations and to successful industrial deployment. Professor Gupta received her Ph.D. in computer science from Carnegie Mellon University in 1994 after earning a master’s degree in computer engineering from Rensselaer Polytechnic Institute and a bachelor’s in electrical engineering from the Indian Institute of Technology in New Delhi."
+
+    giannarakis:
+      name:           Nick Giannarakis
+      site:           https://www.nickgian.github.io
+      avatar:         /assets/images/nick-giannarakis.jpeg
+      bio:            "Nick is a PhD candidate at Princeton University, where he is currently advised by Prof. David Walker. He received a master's degree in Computer Science from ENS Cachan, and a diploma of Electrical and Computer Engineering from National Technical University of Athens."
+      twitter:        naig_kcin
+
+    loehr:
+      name:           Devon Loehr
+      site:           https://dkloehr.github.io
+      avatar:         /assets/images/devon-loehr.jpg
+      bio:            "Devon is a PhD candidate at Princeton University, where he is currently advised by Prof. David Walker. Devon graduated from Swarthmore College in 2018 with High Honors, with majors in Mathematics and Computer Science."
+      
+    thijm:
+      name:           Tim Alberdingk Thijm
+      site:           https://www.cs.princeton.edu/~tthijm/
+      avatar:         /assets/images/tim-thijm.jpg
+      bio:            "Tim is a PhD candidate at Princeton University, where he is currently advised by Prof. Aarti Gupta. Tim completed his BSc at the University of Toronto in 2018 in Computer Science and English."
 
 # Defaults
 defaults:

_posts/2020-05-26-its-the-equivalence-classes-stupid.md

@@ -108,7 +108,7 @@ Most networking people believe this is so because the number of disjoint geometr
 
 There are other twists on equivalence classes. 
 For example, at MSR, we observed that complex data centers had lots of backup links and routers that were essentially similar. 
-While this is classically interpreted as _symmetries_ in the state space, one can view the MSR work as defining equivalence classes on the _topology_; by contrast, Atomic predicates define equivalence classes on the headers. 
+While this is classically interpreted as _symmetries_ in the state space, one can view the [MSR work](https://doi.org/10.1145/2837614.2837657) as defining equivalence classes on the _topology_; by contrast, Atomic predicates define equivalence classes on the headers. 
 
 Again this makes sense because the state for network reachability is a pair __(packet, interface)__ where the __packet__ is the current version of the header (which could be rewritten) and the __interface__ is the interface in the network that the header packet is currently at while traveling from $S$ to $D$.
 While classical work in model checking looks for symmetries/equivalence class on the state space, in networks it makes sense to separately factor the equivalence of states into the equivalence of headers (Yang-Lam) and equivalence of interfaces. 
@@ -122,7 +122,7 @@ But the bigger problem that remains even for dataplane verification is the _lack
 I will write about that in a post called "Look Ma, no specs" about some work to address this problem at UCLA.
 
 There are other ways to reduce time to navigate large state spaces. 
-We can use _[modularity](http://localhost:4000/toward-modular-network-verification/)_ as [Todd Millstein](http://web.cs.ucla.edu/~todd/) points out where the state space is factored into smaller pieces, each with a smaller state space. Second, we can use _abstraction_: we transform the original network state space into a more abstract state space at the price of losing the ability to verify some properties. For example, Minesweeper abstracts away message passing of routing messages using solutions to the Stable Paths Problem.
+We can use _[modularity](../toward-modular-network-verification/)_ as [Todd Millstein](http://web.cs.ucla.edu/~todd/) points out where the state space is factored into smaller pieces, each with a smaller state space. Second, we can use _abstraction_: we transform the original network state space into a more abstract state space at the price of losing the ability to verify some properties. For example, Minesweeper abstracts away message passing of routing messages using solutions to the Stable Paths Problem.
 While modularity and abstraction are essential in other domains, perhaps precomputed equivalence classes are so successful in networks because networking is a shallower (not to mention finite) domain compared to programs or hardware.
 
 I once described networking verification to [Ed Clarke](https://www.cs.cmu.edu/~emc/). His main question was: _what is the state?_ (the (header, packet) pair described above).