Approximating the domains of functional and imperative programs

This paper deals with automated termination analysis of partial functional programs, that is, of functional programs which do not terminate for some input. We present a method to determine their domains (respectively non-trivial subsets of their domains) automatically. More precisely, for each functional program a termination predicate algorithm is synthesized that only returns true for inputs where the program is terminating. To ease subsequent reasoning about the generated termination predicates we also present a procedure for their simplification. Finally, we show that our method can also be used for automated termination analysis of imperative programs.