Patent ID: 9152543
Filing Date: 2015-10-06
Classification: G06F

Abstract:
1. A method of testing software, the method comprising: generating a symbolic value for a return value of a software function of a software program during mixed symbolic and abstraction execution (“mixed execution”) of the software program, one or more paths of the software function including the return value, the mixed execution maintaining symbolic values, abstract values, and constraints of one or more variables of the software function; deriving, during the mixed execution, an abstraction for the symbolic value based on the return value of the one or more paths satisfying the abstraction, the abstraction constraining the symbolic value; generating an assumption for the symbolic value in the software program based on the abstraction such that the assumption constrains the symbolic value; generating a declarative function based on the symbolic value as constrained by the assumption and based on the software function; and exploring, during the mixed execution, the one or more paths of the software function that correspond to the return value based on the symbolic value as constrained by the abstraction by executing the declarative function such that a number of the one or more paths explored during the symbolic execution is constrained by the abstraction, the execution of the declarative function being delayed until the symbolic execution reaches an end of a path of the software program.