Symbolic Execution: The major idea behind symbolic execution (King 1976; Clarke 1976) is to utilize symbolic values, rather than actual data, as input values and to symbolize the values of program variables as symbolic expressions. As an outcome, the outputs evaluated by a program are stated as a function of the symbolic inputs. The state of a symbolically executed program comprises the symbolic values of the program variables, a path condition (abbreviated as PC), and a program counter.
The path condition is a quantifier free boolean formula over the symbolic inputs: it accumulates constraints that the inputs should satisfy in order for an execution to follow the specific associated path. The program counter states the next statement to be executed. A symbolic execution tree characterizes the execution paths followed throughout the symbolic execution of a program. The nodes symbolize program states and the arcs symbolize transitions between states.