1. A method of verifying software, the method comprising: receiving a portion of a software program that includes a plurality of functions; clustering the functions into two or more clusters of functions; generating a symbolic driver for each of the clusters of functions such that multiple symbolic drivers are generated; symbolically executing the clusters of functions using the symbolic drivers to generate concrete test cases for the functions in the clusters; and in response to coverage of the symbolic execution of the clusters of functions being less than a particular coverage or a number of the concrete test cases being more than a particular number of concrete test cases, re-clustering the functions.