21. The computing device of claim 20 , wherein the computing device: incrementally refines and extends a sequence of sets of invariants representing bounded invariants and determines a relevance of the one or more design components referenced in the invariant clauses by executing code that causes the computing device to: evaluate, 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 assign relative priorities to one or more design components referenced in the invariant based on the specific timestep at which the unbounded invariant is introduced; determine 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, identify the design component as a cutpoint and replace the design component with the cutpoint within the abstracted design.
23. The computing device of claim 21 , wherein the computing device assigns relative priorities to one or more design components by executing code which causes 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 an unbounded invariant; in response to the next invariant being an unbounded invariant, automatically update the priority value of each design component referenced within the next invariant to reflect a highest priority; and in response to the next invariant identified being a new bounded 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 bounded invariant; and in response to the resultant value being less than the previously assigned priority value for a design component referenced by the new bounded invariant, update a priority value assigned to the design component referenced by the new bounded invariant to the resultant value.