The ISearcher module is the heart of Bogor's model checking infrastructure. The lifetime of its search() method's execution encompasses the entirely of the state space traversal: initial state creation, transition execution, backtracking, and counterexample creation all occur within its lifetime.