Skip to content

Commit 54d81d1

Browse files
authored
fix link
1 parent 313bc87 commit 54d81d1

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ But the bigger problem that remains even for dataplane verification is the _lack
122122
I will write about that in a post called "Look Ma, no specs" about some work to address this problem at UCLA.
123123

124124
There are other ways to reduce time to navigate large state spaces.
125-
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.
125+
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.
126126
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.
127127

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

0 commit comments

Comments
 (0)