Automatische Terminierungsanalyse (WS 2008/2009)

Seminar: Automatische Terminierungsanalyse
(S2, WS 2008/2009)
LuFG Informatik 2

Veranstalter

Prof. Dr. Jürgen Giesl, Fabian Emmes, Carsten Fuhs, Carsten Otto, Peter Schneider-Kamp, Stephan Swiderski

Voraussetzungen

Kenntnisse in "Logikprogrammierung", "Funktionaler Programmierung", "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).

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).

Termine

Das Seminar wird als Blockseminar im Februar 2009 veranstaltet. Es gelten die folgenden strikten Fristen:

07. 11.: Literatur abholen und besprechen
01. 12.: Besprechung der Konzeption
19. 12.: Abgabe der 1. Version der Ausarbeitung
05. 02.: Kopien der überarbeiteten Ausarbeitung 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. Sollte die Ausarbeitung mehr als fünf Rechtschreib- oder Grammatikfehler auf einer Seite oder mehr als zehn insgesamt enthalten, wird die Bearbeitung abgebrochen.

Themen

Datum	Zeit	Thema	Betreuer	Referent(in)
09.02.	10:40	Recursive Path Orders	S. Swiderski	Helge Stasch
09.02.	11:20	Polynomial Orders	C. Otto	Lukas Razik
09.02.	13:00	Matrix Orders	C. Fuhs	Niklas Hoppe
09.02.	13:40	Termination by Bounded Increase	S. Swiderski	Michael Ernst
10.02.	10:00	Matchbounds	C. Otto	Martin Peter Mrozek
10.02.	10:40	Root Labeling	S. Swiderski	Benjamin Brink
10.02.	11:20	Context-Sensitive Term Rewriting	F. Emmes	Wei Wu
10.02.	13:00	Dependency Pairs for Rewriting with Built-in Numbers	C. Fuhs	Sebastian Schöppel
10.02.	13:40	Certified Termination	C. Fuhs	Patrick Schlebusch
10.02.	14:20	Shallow Dependency Pairs for Isabelle	C. Fuhs	Ergang Song
11.02.	10:00	The Size-Change Principle	J. Giesl	Zhen Xi
11.02.	10:40	Calling Context Graphs	F. Emmes	Christian von Essen
11.02.	11:20	Termination Analysis for Haskell Programs	S. Swiderski	Marc Brockschmidt
11.02.	13:00	Termination Analysis for Prolog Programs via Transformations	J. Giesl	Louis Bertrand Fogang
11.02.	13:40	Dependency Triples for Prolog	J. Giesl	Arikan Can Ates
11.02.	14:20	Termination Analysis for Java Bytecode	C. Otto	Sebastian Biallas
11.02.	15:00	Termination Analysis for C Programs	C. Otto	Sebastian Fillinger

Die Vortragsdauer beträgt 25 Minuten. Alle Zeiten sind vorläufig.

Rückfragen

Bei Fragen wenden Sie sich bitte an Carsten Fuhs.

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik