1. A computer implemented method of verifying whether a correctness property of a design holds true by using a sequential model of the design having a number of reachable control states and data states, said method comprising the steps of: generating a transformed model having fewer reachable control states for at least one depth, while preserving the correctness property and the total number of reachable control states; statically determining which of the reduced number of control states are reachable at each depth in the transformed model; and performing a verification on the transformed model using the statically determined reachable control states; determining the correctness of the model with respect to the said property.