Copenhagen Programming Language Seminar

Automated Termination Analysis of Programs using Dependency Pairs

Peter Schneider-Kamp

Wednesday, November 4th, 2009, 15:00-16:00
The IT University, Rued Langgaards Vej 7, DK-2300, Room Auditorium 3


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)

Scientific host: Carsten Schuermann Administrative host:Renée Korver Michan. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org