1. A method for verifying a property of a complete model of a system under study, the model defining states of the system based on a set of state variables and a transition relation among the states, the method comprising: abstracting at least some of the variables from the model so as to produce an abstract model of the system; beginning with an initial state in a state space of the abstract model, finding an abstract path through the state space of the abstract model in accordance with the transition relation to a target state defined by the property; restoring a subset of the abstracted variables to the abstract model so as to produce an intermediate model of the system; and verifying the property on the complete model based on the intermediate model.