Automatische Terminierungsanalyse (WS 2011/12)

Seminar:
Automatische Terminierungsanalyse
(S2, WS 2011/12)
LuFG Informatik 2

Veranstalter

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

Inhalt

Terminierung ist eine grundlegende Eigenschaft von Programmen und der Nachweis der Terminierung ist eine wichtige Fragestellung im Bereich der Software-Entwicklung und der Programmverifikation. In dem Seminar werden verschiedene Techniken und Tools vorgestellt, um die Terminierung von Programmen automatisch zu untersuchen. Hierbei betrachten wir unterschiedliche Arten von Programmiersprachen (z.B. Termersetzungssysteme, logische, funktionale, und imperative Programmiersprachen).

Voraussetzungen

Kenntnisse in "Funktionaler Programmierung", "Logikprogrammierung", "Termersetzungssystemen" oder "Automatisierter Programmverifikation". Bitte geben Sie bei der Anmeldung an, welche dieser Vorlesungen Sie besucht haben (am besten mit aktiver Teilnahme an den Übungen).

Termin

Das Seminar findet zu Beginn der Semesterferien am 03.02.2012 und 06.02.2012 als Blockseminar statt.

Es gelten die folgenden strikten Fristen:

21.10.2011: Literatur abholen und besprechen
21.11.2011: Besprechung der Konzeption
20.12.2011: Abgabe der 1. Version der Ausarbeitung
30.01.2012: Folien besprechen
vor dem ersten Vortragstag: Kopien der überarbeiteten Ausarbeitung und ggf. Folien für OHP anfertigen

Vorgaben

Die Ausarbeitung darf nicht mehr als 10 Seiten inklusive Titel und Literaturverzeichnis umfassen. Bei diesem Umfang sind weder ein Index noch ein Inhaltsverzeichnis erwünscht, allerdings sollte ein Literaturverzeichnis vorhanden sein. Die Ausarbeitung kann auf Englisch oder auf Deutsch verfasst werden. Sollte die Ausarbeitung mehr als fünf Rechtschreibfehler auf einer Seite oder mehr als zehn insgesamt enthalten, wird die Bearbeitung abgebrochen. Verwenden Sie daher sowohl für Ihre Ausarbeitung als auch für Ihre Folien eine automatische Rechtschreibprüfung!

Themen

Datum	Zeit	Thema	Betreuer	Referent(in)
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

Das Seminar findet voraussichtlich im Seminarraum des Lehrstuhls für Informatik 2 (Gebäude E2, Raum 4201b) statt. Die Vortragsdauer beträgt 25 Minuten, und als Vortragssprache sind Englisch oder Deutsch möglich.