1. A computer-implemented method for verifying the correctness of a software program comprising steps of: by using a computer generating a sequential model of the software program, said sequential model having a number of reachable control states and data states; balancing reconvergent control paths in the sequential model by inserting control states with no data operations in said control paths, wherein balancing comprises matching the number of control states in the respective control paths, generating a transformed model from the sequential model of the software program with one or more balanced reconvergent control paths such that the transformed model has fewer reachable control states for at least one depth, while preserving the correctness property and the total number of reachable control states; determining statically, for the transformed model, which one(s) of its control states are reachable at each depth of the model; performing a bounded model checking (BMC) verification on the sequential model using the statically determined control state information as constraints to the BMC; determining a correctness property of the sequential model; and outputting an indication of that correctness determination.