Gert Smolka: Doctoral Students

Gert Smolka: Doctoral Students

Saarland University Computer Science


Fabian Kunze

Dominik Kirst

Yannick Forster


  1. Kathrin Stark, 2020
    Mechanising Syntax with Binders in Coq.

  2. Steven Schäfer, 2019
    Engineering of Formal Systems in Constructive Type Theory.

  3. Jonas Kaiser, 2019
    Formal Verification of the Equivalence of System F and the Pure Type System L2.

  4. Sigurd Schneider, 2018
    A Verified Compiler for a Linear Imperative/Functional Intermediate Language.
    (Co-supervisor: Sebastian Hack)

  5. Christian Doczkal, 2016
    A Machine-Checked Constructive Metatheory of Computation Tree Logic.

  6. Mark Kaminski, 2012
    Incremental Decision Procedures for Modal Logic with Nominals and Eventualities.

  7. Mathias Möhl, 2010,
    Dynamic Programming based RNA Pseudoknot Alignment.

  8. Guido Tack, 2009,
    Constraint Propagation -- Models, Techniques, Implementation.
    Won ACP Doctoral Research Award 2010.

  9. Marco Kuhlmann, 2007,
    Dependency Structures and Lexicalized Grammars.
    Won E.W. Beth Dissertation Prize 2008.

  10. Andreas Rossberg, 2007,
    Typed Open Programming.

  11. Leif Kornstaedt, 2006,
    Design and Implementation of a Programmable Middleware.

  12. Ralph Debusmann, 2006,
    Extensible Dependency Grammar --- A Modular Grammar Formalism Based On Multigraph Description.

  13. Alexander Koller, 2004,
    Constraint-based and Graph-based Resolution of Ambiguities in Natural Language.

  14. Tim Priesnitz, 2004,
    Subtype Satisfiability and Entailment.
    (Co-supervisor: Joachim Niehren)

  15. Katrin Erk, 2002,
    Parallelism Constraints in Underspecified Semantics.

  16. Tobias Müller, 2001,
    Constraint Propagation in Mozart.

  17. Christian Schulte, 2000,
    Programming Constraint Services.

  18. Michael Mehl, 1999,
    The Oz Virtual Machine: Records, Transients, and Deep Guards.

  19. Ralf Scheidhauer, 1999,
    Design, Implementierung und Evaluierung einer virtuellen Maschine für Oz.

  20. Joachim Paul Walser, 1998,
    Domain-independent Local Search for Linear Integer Optimization.

  21. Martin Müller, 1998,
    Set-based Failure Diagnosis for Concurrent Constraint Programming.

  22. Jörg Würtz, 1998,
    Lösen kombinatorischer Probleme mit Constraintprogrammierung in Oz.

  23. Martin Henz, 1997,
    Objects in Oz.

  24. Joachim Niehren, 1995,
    Funktionale Berechnung in einem uniform nebenläufigen Kalkül mit logischen Variablen.

  25. Rolf Backofen, 1994,
    Expressivity and Decidability of First-order Languages over Feature Trees.

  26. Andreas V. Hense, 1994,
    Polymorphic Type Inference for Object-oriented Programming Languages.


Ezgi Çiçek, 2017, Saarland University.
Relational Cost Analysis.

Fritz Müller, 2016, Saarland University.
On Confluence and Semantic Full Abstraction of Lambda Calculus Languages.

Denis Firsov, 2016, Tallinn University of Technology.
Certification of Context-Free Grammar Algorithms.

Beta Ziliani, 2015, Saarland University.
Interactive Typed Tactic Programming in the Coq Proof Assistant.

Guillaume Hoffmann, 2010, Nancy-Université.
Reasoning Tasks for Hybrid Logics.

Daniel Gorín, 2009, Universidad de Buenos Aires and Nancy-Université.
Resolution-based automated reasoning techniques for hybrid logics.

Eyad Alkassar, 2009, Saarland University.
OS Verification Extended -- On the Formal Verification of Device Drivers and the Correctness of Client/Server Software.

Yevgeny Kazakov, 2005, Saarland University.
Saturation-Based Decision Procedures for Extensions of the Guarded Fragment.

Sven Thiel, 2004, Saarland University.
Efficient Algorithms for Constraint Propagation and for Processing Tree Descriptions.

Andreas Meier, 2003, Saarland University.
Proof Planning with Multiple Strategies.

Serge Autexier, 2003, Saarland University.
Hierarchical Contextual Reasoning.

Christoph Jung, 1999, Saarland University.
Theory and Practice of Hybrid Agents.

Jörg Müller, 1995, Saarland University.
An Architecture for Dynamically Interacting Agents.

Sverker Janson, 1994, Uppsala University.
AKL--A Multiparadigm Programming Language.

Delia Kesner, 1993, Université Paris-Sud, Orsay.
La définition de fonctions par cas à l′aide de motifs dans des langages applicatifs.

Werner Nutt, 1993, Saarland University.
Algorithms for Constraints in Deduction and Knowledge Representation.

Matthias Hecking, 1993, Saarland University.
Eine logische Behandlung der verteilten und mehrstufigen Planerkennung.

Ralf Treinen, 1991, Saarland University.
Modulare Datentypdefinitionen und ihre Beziehungen zur Logik erster Stufe.

Legal notice, Privacy policy