Patent ID: 9454347
Filing Date: 2016-09-27
CPC Classification: G06F

Claim Text:
1. A method of analyzing an incomplete software program, the method comprising: receiving high-level software code of a software program that includes a plurality of functions, the plurality of functions including at least one incomplete function and at least one complete function; compiling at least a portion of the high-level software code to generate low-level software code in symbolic form by compiling the complete function and passing over the incomplete function, the symbolic form including representing variables in the high-level software code as symbolic variables that when symbolically executed are represented by symbolic expressions without a defined value; after generating the low-level software code with the incomplete function, modifying the low-level software code with a symbolic variable to account for a call to the incomplete function in the low-level software code, the symbolic variable being a variable type that is the same as a variable type of a return value of the incomplete function and the symbolic variable not being defined in the high-level software code; symbolically executing the modified low-level software code, the symbolic execution of the symbolic variable resulting in a symbolic expression without a defined value that is part of a symbolic path condition generated during the symbolic execution, the symbolic expression not defined in the high-level software code or the low-level software code; and solving the symbolic path condition, which includes the symbolic expression resulting from the symbolic variable, using a constraint solver.