# US 2017/0286271 A1 · Symbolic execution of alternative branches > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 2017/0286271 A1 - Document ID: US20170286271A1 - Status: Published application - Kind: A1 - Application number: 15/084,617 - Filed: 2016-03-30 - Published: 2017-10-05 - Earliest claimed: 2016-03-30 - Assignees: International Business Machines Corporation - Applicants: International Business Machines Corporation - Inventors: Dmitry Pidan; Tatyana Veksler - Web page: https://patentgrep.com/patent/US20170286271A1 ## CPC - G06F 11/3668: Testing of software - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F 11/3688: {for test execution, e.g. scheduling of test suites} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract Method, apparatus and product for symbolic execution of alternative branches. The method comprising reaching, during symbolic execution of a Control Flow Graph (CFG) of a program, 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. The method further comprises symbolically executing the first branch using the first symbolic state so as to determine a second symbolic state. The method further comprises symbolically executing the second branch using the second symbolic state so as to determine a third symbolic state. Accordingly, the third symbolic state is based on sequential symbolic execution of alternative branches ## Claims ### Claim 1 A computer-implemented method 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, the 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; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined; and symbolically executing the second branch using the second symbolic state, whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches. ### Claim 2 (depends on 1) The computer-implemented method of claim 1, wherein the first branch comprises an assignment instruction, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect a conditional assignment in accordance with the assignment instruction that is conditioned on the first branching condition. ### Claim 3 (depends on 2) The computer-implemented method of claim 2, wherein the assignment instruction is an assignment instruction to a variable having a definition scope that extends beyond the first branch. ### Claim 4 (depends on 2) The computer-implemented method of claim 2, wherein the first branch comprises a second assignment instruction to a local variable, wherein the local variable having a definition scope that is internal to the first branch, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect an unconditional assignment in accordance with the second assignment instruction. ### Claim 5 (depends on 2) The computer-implemented method of claim 2, wherein the second branch comprises a second assignment instruction, wherein the second branch is taken under a second branching condition, wherein said symbolically executing the second branch comprises updating the second symbolic state to reflect a conditional assignment in accordance with the second assignment instruction that is conditioned on the second branching condition. ### Claim 6 (depends on 1) The computer-implemented method of claim 1, wherein the first branch comprises an instruction having a side effect external to the first branch, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect execution of the instruction conditioned on the first branching condition. ### Claim 7 (depends on 1) The computer-implemented method of claim 1 further comprising: upon reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches. ### Claim 8 (depends on 7) The computer-implemented method of claim 7, wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state. ### Claim 9 (depends on 1) The computer-implemented method of claim 1 further comprises: detecting the joining node, wherein said detecting comprises identifying a cut in a subset of the CFG beginning in the branching node that has a cut size of one. ### Claim 10 (depends on 1) The computer-implemented method of claim 1, wherein the symbolic execution of the computer program is a concolic execution of the computer program comprising a symbolic state and a concrete state. ### Claim 11 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; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined; and symbolically executing the second branch using the second symbolic state, whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches. ### Claim 12 (depends on 11) The apparatus of claim 11, wherein the first branch comprises an assignment instruction, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect a conditional assignment in accordance with the assignment instruction that is conditioned on the first branching condition. ### Claim 13 (depends on 12) The apparatus of claim 12, wherein the assignment instruction is an assignment instruction to a variable having a definition scope that extends beyond the first branch. ### Claim 14 (depends on 12) The apparatus of claim 12, wherein the first branch comprises a second assignment instruction to a local variable, wherein the local variable having a definition scope that is internal to the first branch, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect an unconditional assignment in accordance with the second assignment instruction. ### Claim 15 (depends on 12) The apparatus of claim 12, wherein the second branch comprises a second assignment instruction, wherein the second branch is taken under a second branching condition, wherein said symbolically executing the second branch comprises updating the second symbolic state to reflect a conditional assignment in accordance with the second assignment instruction that is conditioned on the second branching condition. ### Claim 16 (depends on 11) The apparatus of claim 11, wherein the first branch comprises an instruction having a side effect external to the first branch, wherein the first branch is taken under a first branching condition, wherein said symbolically executing the first branch comprises updating the first symbolic state to reflect execution of the instruction conditioned on the first branching condition. ### Claim 17 (depends on 11) The apparatus of claim 11, wherein said processor is further adapted to perform: upon the symbolic execution reaching the branching node, dynamically determining to perform sequential symbolic execution of the alternative branches. ### Claim 18 (depends on 17) The apparatus of claim 17, wherein said dynamically determining comprises determining that the first branch and the second branch are feasible according to the first symbolic state. ### Claim 19 (depends on 11) The apparatus of claim 11, wherein the symbolic execution of the computer program is a concolic execution of the computer program comprising a symbolic state and a concrete state. ### Claim 20 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; symbolically executing the first branch using the first symbolic state, whereby a second symbolic state is determined; and symbolically executing the second branch using the second symbolic state, whereby a third symbolic state is determined, the third symbolic state is based on sequential symbolic execution of alternative branches.