I. Introduction
Internet-scale services ranging from search, advertisement, and social networks require stringent performance and availability guarantees from the underlying networks. Yet managing a network at scale is inherently difficult, especially under uncertainties such as failures and dynamic traffic. In this regard, various verification tools have been developed to verify that certain important properties can be guaranteed in the network. Most of them focus on verifying qualitative properties that are path-related [4], [15], [25], [32], e.g., reachability [32], path isolation (two paths do not share any links) [25], waypointing (traffic traverses a chain of services) [4], etc.