tion rule. Instead, stateful SFC verification requires a new forwarding abstraction to consider the disparate state for individual flows (or connections). Second, while verifying the functionality of one NF is tractable, networks consist of many NFs that are chained together. To verify a service chain, a framework must verify not just one NF but all NFs and switches that the flows will traverse: essentially, verifying the entire network. While verifying stateless network devices is already challeng- ing [74, 110], adding stateful devices further complicates the problem. Thus, care must be taken to ensure that verification includes accurate and scalable algorithms that can be applied to realistic networks. It is the simple switch forwarding abstraction, for example, Open- Flow, that makes the data plane verification feasible [110] as it hides the complexity in control plane and represents a unified interface to the verification. In the context of NFV, unfortunately there is no such sim- ple abstraction to capture the data plane behavior of an NF. Inspired by the OpenFlow match-action abstraction, we can use a new NF for- warding abstraction. It comprises of two parts: a match-action table and a state machine. The state machine is a natural representation of stateful processes. The nodes in the state machine are the states each NF maintains, and the edges capture the conditions that trigger state transitions. The table contains match-action rules: matching on both the packet header and the internal states, performing the action on packets, and changing the internal states. Illustration of the stateful table is shown in Figure 5.13. Use expert knowledge or by talking with network operators, we can determine the state machines for the NFs. We observe that all existing verification tools build some form of for- warding graphs from the rules and then perform reachability checks on this graph [110], as graph traversal algorithms are efficient and scal- able. However, this approach is insufficient for our problem because