Master and Diploma Theses, Programming Systems Lab, Prof. Gert Smolka

If you are interested in a topic for a thesis, please contact Prof. Smolka or a researcher of the Lab whose work you find interesting.

As part of your thesis work, you will participate in our Graduate Seminar. You will give two talks in your seminar phase and one final talk after submitting your thesis. The first and second talk are 20 minutes each, the final talk is 30 minutes, always plus discussion time.

When you start your thesis work, your advisor will provide you with a problem specification (1 page). You will maintain a web page devoted to your thesis work. The problem specification, the thesis and related software and documentation will be made available through this page (see examples below).

Since 2001, FdSI annually awards the Günther-Hotz-Medaille to the best graduates of the Master Program. So far, 5 students with theses advisors from our lab won: Manuel Bodirsky (2001), Jan Schwinghammer (2002), Guido Tack (2003), Mark Kaminski (2006), and Cătălin Hriţcu (2007). Who will be the next?

Thesis Projects in Progress

Julian Backes, 2009,
Tableaux for Higher-Order Logic with If-Then-Else, Descriptions and Choice (Advisor: Brown)

Christine S. Rizkallah, 2008,
Proof Representations for Higher-Order Logic (Advisor: Brown)

Thesis Projects Completed

Christian Doczkal, 2009,
Formalizing TT-lifting in Isabelle/HOL-Nominal (Advisor: Schwinghammer)

Daniel Götzmann, 2009,
A Tableau Prover for Hybrid Logic (Advisor: Kaminski)

Niko Paltzer, 2007,
Infrastructure and Tools for Debugging Constraint Propagation (Advisor: Tack)

Cătălin Hriţcu, 2007, won Günther-Hotz-Medaille
Step-indexed Semantic Model of Types for the Functional Object Calculus (Advisor: Schwinghammer)

Patrick Pekczynski, 2007,
Domain approximations for finite set constraint variables: An integrated approach (Advisor: Tack)

Mark Kaminski, 2006, won Günther-Hotz-Medaille and Preis der Kühborth-Stiftung
Completeness Results for Higher-Order Logic (Advisor: Smolka)

Murat Baktiev, 2006,
Permutation Semantics of Separation Logic (Advisor: Schwinghammer)

Matthias Horbach, 2006,
Cut Elimination via Splitting versus Cut Elimination via Proof Nets (Advisor: Straßburger)

Robert Grabowski, 2006,
Computational Aspects of Non-Projective Dependency Grammars (Advisor: Kuhlmann)

Christian Müller, 2006,
Run-time Byte Code Compilation, Optimization and Interpretation for Alice (Advisor: Tack)

Mathias Möhl, 2006,
Drawings as Models of Syntactic Structure: Theory and Algorithms (Advisor: Kuhlmann)

Patrick Cernko, 2004,
Realisierung einer Java Virtual Machine mit SEAM (Advisor: Brunklaus)

Guido Tack, 2003, won Günther-Hotz-Medaille and VDI-Preis
Transformation, Linearization and Minimization of Data Graphs with Transients (Advisors: Smolka, Kornstaedt)

Dag Kröper, 2002,
Konzeption und Realisierung eines Bibliotheksverwaltungssystems (Advisors: Schulte, Smolka)

Martin Homik, 2002,
Ressourcenoptimierung eines Workflowproblems (Advisors: Schulte, Müller)

Jan Schwinghammer, 2002, won Günther-Hotz-Medaille
A Concurrent Lambda-Calculus with Promises and Futures (Advisors: Niehren, Smolka)

Ralph Debusmann, 2001,
A Declarative Grammar Formalism For Dependency Grammar (Advisor: Duchier)

Manuel Bodirsky, 2001, won Günther-Hotz-Medaille
Beta Reduction Constraints (Advisor: Niehren),

Gerhard Schneider, 2000,
ML mit Typklassen (Advisors: Rossberg, Kornstaedt)

Thorsten Brunklaus, 2000,
Der Oz Inspector - Browsen: Interaktiver, einfacher, effizienter (Advisor: Schulte)

Tim Priesnitz, 2000,
Entailment von nicht-strukturellen Teiltyp-Constraints (Advisor: Niehren)

Daniel Simon, 1999,
An Implementation of the Programming Language DML in Java: Runtime Environment (Advisor: Kornstaedt)

Andy Walter, 1999,
An Implementation of the Programming Language DML in Java: Compiler (Advisor: Kornstaedt)

Alexander Koller, 1999,
Constraint Languages for Semantic Underspecification (Advisor: Niehren)

Benjamin Lorenz, 1998,
Ein Debugger für Oz (Advisors: Kornstaedt, Scheidhauer)

Leif Kornstaedt, 1996,
Definition und Implementierung eines Front-End-Generators für Oz (Advisor: Schulte)

Kai Ibach, 1995,
OzFun: Eine funktionale Sprache für gemischte Eager- und Lazy-Programmierung (Advisor: Niehren)

Frank Zenner, 1995,
Anbindung einer grafischen Benutzerschnittstelle an Oz (Advisors: Mehl, Scheidhauer)

Bernhard Latz, 1994,
Eine interaktive Benutzerschnittstelle für Oz (Advisor: Smolka)

Stefan Jacobs, 1993,
Über Negation im logischen Programieren (Advisor: Smolka)

Markus Höhfeld, 1988,
Ein Schema für constraint-basierte relationale Wissensbasen (Advisor: Smolka, Uni KL)

Michael Schmitt, 1987,
Implementierung einer typisierten logischen Programmiersprache mit Gleichheit (Advisor: Smolka, Uni KL)

Gert Smolka ()