Patent ID: 7360186

Claim:
A method for invariant checking, the method comprising: executing one or more first steps of a finite state machine (FSM) corresponding to one or more binary decision diagrams (BDDs) to traverse a state space of the FSM in a first direction with respect to an initial state and an erroneous state; automatically and without user input, accessing a first profile corresponding to the one or more first steps of the FSM; automatically and without user input, comparing the first profile with one or more first predetermined criteria; automatically and without user input, stopping the traversal of the state space in the first direction according to the comparison between the first profile and the one or more first predetermined criteria; automatically and without user input, executing one or more second steps of the FSM to traverse the state space in a second direction with respect to the initial state and the erroneous state opposite the first direction according to a first partial result from the one or more first steps of the FSM; automatically and without user input, accessing a second profile corresponding to the one or more second steps of the FSM; automatically and without user input, comparing the second profile with one or more second predetermined criteria; automatically and without user input, stopping the traversal of the state space in the second direction according to the comparison between the second profile and the one or more second predetermined criteria; and automatically and without user input, executing one or more third steps of the FSM to traverse the state space in the first direction from the one or more first steps according to a second partial result from the one or more second steps of the FSM.