12. The computer program product of claim 11 , further comprising program code configured to cause the computing device to: incrementally refine and extend a sequence of sets of invariants representing bounded invariants and determine a relevance of the one or more design components referenced in the invariant clauses by: evaluating, for each invariant, whether the invariant is an unbounded invariant that is first introduced at a specific timestep between the initial and the kth timestep; deterministically assigning relative priorities to one or more design components referenced in the invariant based on the specific timestep at which the unbounded invariant is introduced; determining for each design component referenced by an invariant, if the design component has a priority that is equal to a highest priority assigned among the design components; and in response to the design component not having a priority equal to the highest priority assigned, identifying the design component as a cutpoint and replacing the design component with the cutpoint within the abstracted design.
12. The computer program product of claim 11 , further comprising program code configured to cause the computing device to: incrementally refine and extend a sequence of sets of invariants representing bounded invariants and determine a relevance of the one or more design components referenced in the invariant clauses by: evaluating, for each invariant, whether the invariant is an unbounded invariant that is first introduced at a specific timestep between the initial and the kth timestep; deterministically assigning relative priorities to one or more design components referenced in the invariant based on the specific timestep at which the unbounded invariant is introduced; determining for each design component referenced by an invariant, if the design component has a priority that is equal to a highest priority assigned among the design components; and in response to the design component not having a priority equal to the highest priority assigned, identifying the design component as a cutpoint and replacing the design component with the cutpoint within the abstracted design. 15. The computer program product of claim 12 , wherein the program code configured to cause the computing device to assign relative priorities to one or more design components comprises program code configured to cause the computing device to: initially assign to each of the design components a priority value representing a low priority; determine if a next invariant identified is a new invariant; and in response to the next invariant identified being a new invariant: determine a maximum depth (i) to which the next invariant can be propagated forward in the design, where the maximum depth is equivalent to a timestep i, which is less than a bounded timestep j at which the invariant was derived; calculating a resultant value of j-i; determine whether the resultant value is less than a previously assigned priority value for each design component referenced by the new invariant; and in response to the resultant value being less than the previously assigned priority value for a design component referenced by the new invariant, update a priority value assigned to the design component referenced by the new invariant to the resultant value.