Automated Termination Analysis of Programs using Dependency Pairs

EPFL IC Tresor talks

by Peter Schneider-Kamp 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, many of them based on the dependency pair framework developed in the term rewriting 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 for each programming paradigm and language, we want to take advantage of existing powerful tools for automated termination analysis based on the dependency pair framework. In this talk, we describe recent results which permit the reduction of termination problems for declarative programming languages to problems in the dependency pair frame work. We present such approaches for the functional language Haskell and the logic language Prolog. Our results have been implemented in the termination prover AProVE. Our resulting termination analyzers are currently the most powerful ones for both Haskell and Prolog. (Joint work with Jürgen Giesl, René Thiemann, Alexander Serebrenik, Stephan Swiderski, and Thomas Ströder)