-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.
0 commit comments