5th International School on Rewriting

3 – 8 July 2010, Drift 21, Utrecht, Netherlands

Termination of Programs

Lecturer

Peter Schneider-Kamp (University of Southern Denmark, Odense, Denmark)

Introduction

(advanced track, 3 lecture sessions)

The question whether a given program terminates for all its inputs is one of the fundamental problems in program verification. Instead of developing completely new techniques for each programming paradigm and language, in this course we learn how one can take advantage of existing approaches for automated termination analysis of term rewriting.

We first introduce the dependency pair framework for analyzing termination of term rewriting. We then learn how termination problems for programs written in real programming languages can be reduced to termination problems in term rewriting. To this end we use the logic language Prolog, the functional language Haskell, and the imperative language Java.

Material

• zip file of course material (unzips to a directory psk)