A method of implementing a traversal strategy as part of a dynamic verification can include initializing a non-deterministic automaton (NDA) traversal mechanism that has (1) a strategy push-down stack (strategy PDS) that holds traversal strategy pointers and (2) an object push-down stack (object PDS) that holds object pointers, pushing a traversal strategy object pointer onto the strategy PDS, wherein the traversal strategy object pointer points to a traversal strategy object, popping a current object pointer from the object PDS, and determining whether the current object pointer points to a terminal object.