The question whether a given program terminates for all its inputs is one of the fundamental problems in program verification. Thus it has been researched quite thoroughly in the past and many techniques and tools have been developed, most notably in the term rewriting and the logic programming community.
However, until very recently, hardly any of these techniques could be used for real programming languages. Instead of starting from scratch and developing completely new techniques, we want to take advantage of existing powerful tools for the automated termination analysis of term rewrite systems (TRSs).
In this talk, we describe recent results which permit the application of existing techniques from term rewriting in order to prove termination of programs. We discuss two possible approaches:
Translate programs into TRSs and use existing tools to verify termination of the resulting TRSs.
Adapt TRS-techniques to the respective programming languages in order to analyze programs directly.
We present such approaches for the functional language Haskell and the logic language Prolog. Our results have been implemented in the termination provers AProVE and Polytool. Our resulting termination analyzers are currently the most powerful ones for both Haskell and Prolog.
The talk is based on joint work with Danny De Schreye, Jürgen Giesl, Manh Thang Nguyen, Alexander Serebrenik, Stephan Swiderski, and René Thiemann.