1. A method of testing a software program, the method comprising: generating a test driver by assigning concrete values to input variables of the software program; assigning symbolic source set elements to the input variables of the software program; generating source set functions, the source set functions representing a relationship between value storages of the software program and the symbolic source set elements, the source set functions comprising Boolean variables representing the symbolic source set elements, and Boolean operators describing a relationship between the Boolean variables; symbolically executing, with data source analysis, a current instruction of the software program based on the concrete values and symbolic source set elements assigned to the input variables of the software program; and based on the symbolic execution with data source analysis, determining whether the software program meets one or more predetermined requirements; wherein the Boolean variables of the source set functions are first Boolean variables and the Boolean operators of the source set functions are first Boolean operators, and wherein the generating source set functions includes generating an array source set function, the array source set function representing a relationship between values in an array variable of the software program and the symbolic source set elements, the array source set function comprising the first Boolean variables representing the symbolic source set elements, second Boolean variables representing indices of the array variable, and second Boolean operators describing a relationship between the first Boolean variables and the second Boolean variables.