1. A method comprising: by one or more computing devices, symbolically executing a software module having a number of execution paths; and losslessly reducing the number of execution paths during the symbolic execution of the software module.