Automated Termination Analysis of Programs using Term Rewriting

  • Peter Schneider-Kamp | Aachen University

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:

  1. Translate programs into TRSs and use existing tools to verify termination of the resulting TRSs.
  2. 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.

Speaker Details

Peter Schneider-Kamp is a researcher at the RWTH Aachen University in Aachen, Germany. His research interests include topics in program verification, term rewriting, theorem proving, and programming languages.During the last four years, Peter Schneider-Kamp has been working on program termination and is one of the principal authors of the AProVE tool for fully automated termination analysis of logic programs (Prolog), functional programs (Haskell 98), and imperative programs (subset of Java). AProVE was the winning tool of the International Termination Competitions in 2004, 2005, 2006, and 2007.

Watch Next