zu vergebende Arbeiten

• Fortgeschrittenenpraktikum/Bachelorprojekt oder Diplomarbeit
  Effiziente Termrepräsentationen für Typisierungsalgorithmen
  Betreuer:  Dr. Andreas Abel
  Ausschreibungsdatum:  15.06.2010
   
• Fortgeschrittenenpraktikum/Diplomarbeit
  Implementierung eines Typsystems für Objektorientierte Programme
  Betreuer:  Prof. Dr. Martin Hofmann
  Ausschreibungsdatum:  01.07.2009
   

in Bearbeitung

• Fortgeschrittenenpraktikum
  Verifizierte Standardbibliothek für die funktionale Sprache Agda
  Betreuer:  Dr. Andreas Abel
  Ausschreibungsdatum:  01.07.2009
   

abgeschlossene Arbeiten

• Diplomarbeit
  Markus Jehle, März 2008
  Bounded Model Checking for all Regular Properties
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Diplomarbeit
  Karl Mehltretter, Datum?
  Type and Termination Checking Dependent Types
  Betreuer:  Dr. Andreas Abel
   
• Diplomarbeit
  Dulma Rodriguez, Dezember 2007
  Algorithmic Subtyping for Higher-Order Bounded Quantification Revisited
  Betreuer:  Dr. Andreas Abel
   
• Diplomarbeit
  Markus Latte, Dezember 2007
  Towards lower bounds for intuitionistic propositional proofs
  Betreuer:  Prof. Dr. Martin Hofmann,   Dr. Jan Johannsen
   
• Diplomarbeit
  Marie-Fleur Revel, Dezember 2006
  Translating PSL into the linear time mu-calculus
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Diplomarbeit
  Boris Lohner, Dezember 2006
  Vorlesungsumfragen Online
  Betreuer:  Hans Dietmar Jäger, Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Karl Mehltretter, Juni 2006
  Übersetzung zwischen schwachen, alternierenden Paritätsautomaten und dem Linearzeit mu-Kalkül
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Markus Jehle, April 2006
  Bounded Model Checking für den Linearzeit-Mu-Kalkül
  Betreuer:  Priv.-Doz. Dr. Martin Lange,   Dr. Jan Johannsen
   
• Fortgeschrittenenpraktikum
  Anja Feichtner, Susanne Sojer, April 2006
  Paritätsspiele durch Reduktion auf SAT lösen
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Dulma Rodriguez, März 2006
  Verification in Coq of (co-)iteration schemes for higher-order and nested datatypes
  Betreuer:  Dr. Ralph Matthes, Dr. Andreas Abel
   
• Diplomarbeit
  Christian Dax, März 2006
  Games for the Linear Time Mu-Calculus
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Jan Hoffmann, März 2006
  Minimising weak alternating parity automata
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Konstantin Kutzkow, März 2006
  Natural HeapSort - ein neuer adaptiver Sortieralgorithmus
  Betreuer:  Dr. Jan Johannsen
   
• Diplomarbeit
  Roland Axelsson, Januar 2006
  Automated Abstractions for Existential and Universal Properties
  Betreuer:  Prof. Dr. Martin Hofmann
   
• Fortgeschrittenenpraktikum
  Nicolas Rachinsky, Januar 2006
  Untersuchung der Verwendbarkeit von SAT-Solving zur Schulstundenplanung
  Betreuer: Priv.-Doz. Dr. Martin Lange,  Dr. Jan Johannsen  
   
• Diplomarbeit
  Robert Reitmeier, September 2005
  SAT Encoding of Linear Time mu-Calculus and Weak Alternating Parity Automata
  Betreuer: Priv.-Doz. Dr. Martin Lange,  Dr. Jan Johannsen  
   
• Fortgeschrittenenpraktikum
  Elisabeth Laika, Cornelia Stamm, Juli 2005
  Untersuchung der Verwendbarkeit von SAT-Solving zur Schulstundenplanung
  Betreuer:  Dr. Jan Johannsen,   Prof. Dr. Martin Hofmann,
   
• Fortgeschrittenenpraktikum
  Roland Axelsson, 2005
  Optimal Transitions in Abstract State Systems
  Betreuer:  Dr. Ralph Matthes, Prof. Dr. Martin Hofmann
   
• Fortgeschrittenenpraktikum
  Christian Dax, Juni 2004
  Implementation of LTL Focus Games
  Betreuer:  Priv.-Doz. Dr. Martin Lange
   
• Fortgeschrittenenpraktikum
  Robert Reitmeier, März 2004
  Implementierung eines Algorithmus zur Beweissuche im Polynomkalkül
  Betreuer:  Dr. Jan Johannsen
   
• Fortgeschrittenenpraktikum
  Jan Peter Gutzmann, Dezember 2003
  Implementierung eines Type-Checkers für das System F-omega
  Betreuer:  Dr. Andreas Abel
   
• Fortgeschrittenenpraktikum
  Markus Bleicher, Mai 2002
  Typprüfung für System F-omega mit CASE und PAIR
  Betreuer:  Dr. Ralph Matthes