 state and flow fields in the match column as its condition statements and performs the state/flow statements in action column. This program can be viewed as a microservice with the same functionality with the NF, focusing on the logic of NFs. The challenge in model-based NF programming is to guarantee other program requirements, including performance, isolation, and providing management API. The DFA model of NFs lays the foundation of several stateful network verification solutions. While we list two existing DFA-based solutions in previous sections, there are still challenges in stateful network verifications. For example, how to guarantee the complete- ness and soundness of the verification? How to efficiently verify large networks with frequent changes? We are abstracting and solving these problems based on DFA theory. NF models can also be used in service policy composition. When deploying a network-wide policy composed by several NFs, there may be conflicts between NFs. For example, deploying a cache and a fire- wall in different orders would lead to different results, for example, one client's content may be cached and provided to another client, which was intended to be blocked by the firewall. NF models can be used to determine this order in service policy composition; the operator models the input/output of each NF when chaining them, SO that the end-to-end requirements can be guaranteed. VNF Placement VNF placement problem entails choosing where to place instances of VNFs on servers in a physical network in order to accommodate the traffic for a set of service chains. A few examples of VNFs are firewall 3 Network Function Virtualization services, intrusion detection, caches, and proxies. Each service chain is a stream of network packets flowing through a sequence of VNFs at a certain rate. Network traffic for a given service chain must visit the chain's sequence of VNFs in the specified order. In the VNF place- ment problem, one must place (possibly multiple) instances of each VNF on servers and choose