COMPUTER SCIENCE COLLOQUIUM
Automated Termination Analysis of Programs using Term Rewriting
Peter Schneider-Kamp
Department of Computer Science
RWTH Aachen, Germany
Monday, 06 October, 2008 at 10:15
Room U49E
ABSTRACT
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.
SDU HOME |
IMADA HOME |
Previous Page
Daniel Merkle