1. A method comprising: by one or more computing devices, symbolically executing a software module having a number of execution paths; losslessly reducing the number of execution paths during the symbolic execution of the software module; and representing the software module using a Control Flow Graph; wherein losslessly reducing the number of execution paths during the symbolic execution of the software module comprises: identifying a first path condition and a second path condition forming a sequential composition in the Control Flow Graph; performing dependency analysis for the first path condition and the second path condition; determining that the first path condition and the second path condition are independent of each other; and based on the determination that first path condition and the second path condition are independent of each other: converting the sequential composition into an equivalent parallel composition of the first path condition and the second path condition; and ignoring any duplicate path in the parallel composition.