Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups:(1) algorithms with strong behavioral guarantees that work in limited circumstances (eg, complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (eg, Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees?