Symbolic Execution
This is symbolically substituting operations along a path in order to express the predicate solely in terms of the input and constant vectors.
I.E evaluate the program on symbolic input values and use an automated theorem prover to check if corresponding concrete input values make the program fail.
We execute the program on symbolic values where our symbolic state maps variables to symbolic values. The path condition is a logical formula over the symbolic inputs that encodes all branch decisions taken so far. All paths in the program form its execution tree, in which some paths are feasible and some are infeasible.
Example
Here, we consider the values of x and y as we hit each condition, for the different possible configurations of x and y.