Efficient SMT-Based Network Fault Tolerance Verification.

Network control planes are highly sophisticated, resulting in networks that are difficult and error-prone to configure. Although several network verification tools have been developed to assist network operators, they are limited and inefficient in handling fault-tolerance policies. In this paper, we propose a novel SMT encoding to speed up control plane fault tolerance verification by pruning failed topologies. This encoding exploits the observation that the verifier has to check failures only for the links lying on a set of best paths which can be computed by a recursive algorithm. We implemented our technique in Minesweeper, a state-of-the-art SMT-based verifier. Our evaluation shows that the new encoding speeds up verification by the factor of 3.1–26.9X.