All-Termination(T)

---

Panagiotis Manolios and Aaron Turon. TACAS 2009: Tools and Algorithms for the Construction and Analysis of Systems, © Springer Verlag

Abstract

We introduce the All-Termination(T) problem: given a termination solver T and a collection of functions F, find every subset of the formal parameters to F whose consideration is sufficient to show, using T, that F terminates. An important and motivating application is enhancing theorem proving systems by constructing the set of strongest induction schemes for F, modulo T. These schemes can be derived from the set of termination cores, the minimal sets returned by All-Termination(T), without any reference to an explicit measure function. We study the All-Termination(T) problem as applied to the size-change termination analysis (SCT), a PSpace-complete problem that underlies many termination solvers. Surprisingly, we show that All-Termination(SCT) is also PSpace-complete, even though it substantially generalizes SCT . We develop a practical algorithm for All-Termination(SCT), and show experimentally that on the ACL2 regression suite (whose size is over 100MB) our algorithm generates stronger induction schemes on 90% of multiargument functions.

PDF (270K) © Springer Verlag