1. In a computer system, a method of performing test generation for a computer program, the method comprising: generating a Boolean abstraction of the computer program, wherein the generating comprises selecting a set of predicates in the computer program and calculating a set of possible predicate values for plural statements in the computer program, wherein at least one of the predicates is derived from a conditional statement of the computer program; performing a state reachability analysis of the computer program, wherein performing the state reachability analysis comprises identifying a subset of the set of possible predicate values for the plural statements in the computer program, wherein the subset comprises an approximation of reachable states in the computer program, and outputting a set of paths that covers states in the approximation of reachable states; and performing symbolic execution, wherein the symbolic execution determines whether the paths are feasible and generates inputs for the computer program to cover a path when the oath is feasible.