Symbolic execution of alternative branches

An apparatus for performing symbolic execution of a computer program, wherein the symbolic execution traverses a Control Flow Graph (CFG) of the computer program while updating a symbolic state of the computer program, wherein the apparatus comprising a processor being adapted to perform the steps of:

• reaching a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG;
• upon reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches, wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state;
• symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined;
• symbolically executing the second branch using the second symbolic state, wherein the second symbolic state is an outcome of symbolic execution of the first branch using the first symbolic state, wherein the first branch and the second branch are symbolically executed in a sequential manner whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches;
• and
• symbolically executing an instruction at the joining node using a single symbolic state to jointly represent symbolic execution of a first execution path and a second execution path, wherein the first execution path comprises the first branch, wherein the second execution path comprises the second branch.

A computer program product for performing symbolic execution of a computer program, wherein the symbolic execution traverses a Control Flow Graph (CFG) of the computer program while updating a symbolic state of the computer program, wherein the computer program product comprising a computer readable storage medium retaining program instructions, which program instructions when read by a processor, cause the processor to perform a method comprising:

• reaching a branching node in the CFG with a first symbolic state, wherein the branching has at least a first branch and a second branch, wherein the first and second branches end at a joining node in the CFG;
• upon reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches, wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state;
• symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined;
• symbolically executing the second branch using the second symbolic state, wherein the second symbolic state is an outcome of symbolic execution of the first branch using the first symbolic state, wherein the first branch and the second branch are symbolically executed in a sequential manner whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches;
• and
• symbolically executing an instruction at the joining node using a single symbolic state to jointly represent symbolic execution of a first execution path and a second execution path, wherein the first execution path comprises the first branch, wherein the second execution path comprises the second branch.