Previous symbolic software model checkers (i.e., program analysis tools based on predicate abstraction, pushdown model checkiterative counterexample-guided abstraction refinement, etc.) are restricted to safety properties. Terminator is the first software model checker for termination. It is now being used to prove that device driver dispatch routines always return to their caller (or return counterexamples if they if they fail to terminate).