All-Termination(T)

We introduce the All-Termination(T) problem: given a termination solver, T, and a program (a set of functions), find every set of formal arguments whose consideration is sufficient to show the program terminating using T. One important and motivating application is enhancing theorem proving systems by constructing the set of strongest induction schemes for a program, modulo T. These schemes can be derived from the set of termination cores, the minimal sets returned by All-Termination(T). We study the All-Termination(T) problem as applied to two existing termination analyses: general size-change (SCT) and polynomial size-change (SCP). We analyze the intrinsic complexity of the problems and develop algorithms that we expect to perform well in practice. We show that All-Termination(SCT) is a PSpacecomplete problem. We also show that no output-polynomial algorithm exists for AllTermination(SCP) (unless P = NP). Finally, we develop practical algorithms, some based on SAT-solving, for both...

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Panagiotis Manolios, Aaron Turon
• Keywords: Algorithms, Strongest Induction Schemes, TACAS 2009, Termination Solver, Theorem Proving Systems