Automated Termination Analysis (WS 2011/12)

Seminar:
Automated Termination Analysis
(S2, WS 2011/12)
LuFG Informatik 2

Instructor

Prof. Dr. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Carsten Otto, Thomas Ströder

Termination is an essential property of programs and termination analysis is an important task in software development and program verification. In the seminar, we present techniques and tools to prove termination of programs automatically, where we focus on different types of programming languages (e.g., term rewrite systems, logic, functional, and imperative programming languages).

Prerequisites

Participants should have knowledge in "functional programming", "logic programming", "term rewriting", or "program verification". When registering for the seminar, please indicate which of these lectures you have attended (preferably lectures where you also actively participated in the exercises).

Times

The seminar will take place at the end of the semester (Feb 03 2012 and Feb 06 2012).

We have the following deadlines:

Oct 21 2011: Contact your supervisor to obtain and discuss the literature
Nov 21 2011: Understand the content of your literature sources and discuss the conception of your paper with your supervisor
Dec 20 2011: Submit your complete seminar paper
Jan 30 2012: Discuss your slides with your supervisor
before the first day of the talks: Prepare copies of your revised seminar paper and, if needed, of slides for the OHP

Requirements

Your seminar paper should have 10 pages and be written in either English or German. With this number of pages, there should not be any index or table of contents. Nevertheless, you should give a list of your references. If there are more than ten grammatical or spelling mistakes on a single page, the review of your paper will be aborted, and it will be returned to you immediately (please use an automated spell checker!).

Topics

Date	Time	Topic	Supervisor	Student
03.02.	10:00	Dependency Pairs	F. Emmes	Matthias Hoelzel
03.02.	10:45	SAT Solving for Finding Polynomial and Matrix Orders	M. Brockschmidt	Martin Heistermann
03.02.	11:30	String Rewriting and Matchbounds	C. Otto	Christoph Worreschk
03.02.	13:15	Integer Term Rewriting	J. Giesl	Florian Frohn
03.02.	14:00	Termination Analysis for Java Bytecode via Constraint Logic Programming	C. Otto	Thomas Gerlitz
03.02.	14:45	Termination Analysis for Java Bytecode via Term Rewriting	C. Otto	Jens Noschinski
06.02.	11:00	Termination Analysis for C Programs via Term Rewriting	M. Brockschmidt	Sven Förster
06.02.	11:45	Direct Termination Analysis for C Programs	T. Ströder	Mirco Giacobbe
06.02.	13:15	Non-Termination Analysis for C Programs	T. Ströder	Kai Driessen
06.02.	14:00	Size-Change Termination	J. Giesl	Jasper Diesel
06.02.	14:45	Termination Analysis for Haskell	F. Emmes	Devran Ölcer
06.02.	15:30	Termination Analysis for Prolog Programs via Term Rewriting	T. Stroeder	Alexander Roth

The seminar most likely takes place in the seminar room of Computer Science 2 (building E2, room 4201b). The talks should not take more than 25 minutes and can be held in either English or German.

Further Details and Questions

For further details please contact Carsten Otto.

Area

Theoretical Computer Science, Area of Specialization

Disclaimer

Research Group Computer Science 2

Dept. of Computer Science

Seminar: Automated Termination Analysis