ce is to analyze the dependency between program statements. Within one statement in a given program, the value of the left-hand-side (LHS) variable depends on that of the right-hand-side (RHS) variables; and between statements, the value of an RHS variable in a statement depends on the preceding statements where that variable is on the LHS. This depen- dency analysis results in a "static" program slice where all statements in that slice might lead to the final behavior. A "dynamic" program slice is all statements that really lead to the final behavior, which requires exe- cution analysis based on actual variable values [59]. Several research 3.5 NF Modeling projects have improved program slicing techniques - for example, interprocedure slicing and system dependency analysis [60, 61]. Symbolic execution Symbolic execution is another program analysis approach that sub- stitutes one or several program variables by symbolic values. As the program runs, whenever a branch instruction is met, the program is forked and both branches proceed. The program state variables and path constraints are kept by each path individually. At the end of a path's execution, concrete values of symbolic variables are computed according to the path constraints [62, 63]. Symbolic execution can exercise all possible execution paths, but path explosion can happen with a large code base. Various efforts have made symbolic execution practical in NF verification. To reduce the branching factor (number of branches at each branch instruction), Dobrescu and Argyraki [64] and SymNet [56] propose to write NF programs in a style with bounded loops and data structures, and BUZZ [54] constrains the number and scope of symbolic variables. NF state analysis OpenNF [52] is a flow state management framework that enables joint control with SDN and NFV frameworks. An important issue when integrating existing NFs into OpenNF is to identify state variables in NF programs. StateAlyzer [53] defines features of state variables in an NF program, leveraging several 