Bei Fragen wenden Sie sich bitte an die genannten Ansprechpartner (auch unverbindlich). Weitere Themen können in persönlicher Absprache mit den Lehrenden der Abteilung vereinbart werden.

Bachelor- und Masterarbeiten werden individuell nach Absprache vergeben und betreut. Rechtzeitiges Informieren und Bekunden von Interesse sind von Vorteil. Wenden Sie sich an Prof. Olderog (zu den Sprechzeiten) oder gerne auch an seine Mitarbeiter(innen).

• Implementierung eines Tools zur Transformation von MLSLS in SMTLib
  Christian Harken   (September 2017)
   
• Graphischer Editor für Verkehrssituation
  Lasse Hammer   (August 2017)
   
• Sicheres Überholen bei Gegenverkehr totz nicht perfektem Wissen
  Sven Lampe   (Februar 2017)
   
• Überführung von MLSL- zu QdL-Formeln
  Christopher Bischopink   (Oktober 2016)
   
• Existenzgraphen: werkzeuggestützte Anwendung von Schlussregeln
  Sebastian Schmidt   (Oktober 2014)
   
• Graphischer Editor für Constraint-Diagramme und Übersetzung nach PLC-Automaten
  Nils Hobbensiefken   (August 2014)
   
• Reguläres Model-Checking für parametrisierte Phasen-Event-Automaten mittels Widening
  Carolin Radig   (Juli 2014)
   
• Implementierung eines Diagrammeditors für Shape-Diagramme in Eclipse
  Sören Dierkes   (April 2012)

• Erweiterung der Transformation von Duration Calculus in Phasen-Event-Automaten mit Intergratoren
  Heinrich Ody   (Oktober 2011)
   

• Entwicklung einer Verifikationsumgebung für eine dynamisch getypte Programmiersprache
  Dennis Kregel   (Dezember 2015)
   
• Petri-Spiele: Erweiterung der Sicherheitsgewinnbedingungen auf Markierungen
  Valentin Spreckels   (August 2015)
   
• Entwicklung eines Editors zur Erstellung von PLC-Automata in Eclipse mit Unterstützung des Theorembeweisers Z3
  Sören Dierks   (September 2014)
   
• Refinement of PI-calculus processes
  Manuel Gieseking  (März 2014)
   
• Semantik von Controllern für sichere Fahrzeugmanöver
  Maike Schwammberger   (Januar 2014)
   

• Implementierung einer Übersetung der strukturellen Logik PSTL auf Pi-Kalkül-Prozessen in LTL auf Petrienetzen
  Sören Jeserich   (September 2011)
   
• Entwicklung eines Verification Managers für Syspect
  Jannis Stachowiak   (Juni 2010)
   
• Reguläres Model-Checking für parametrisierte Phasen-Event-Automaten [pdf]
  Boris Rosenow   (März 2010)
   
• Erweiterung von Syspect um einen Editor für Phasen-Event-Automaten [pdf]
  Matthias Peters   (Oktober 2009)
   
• Werkzeuge für Bisimulationsäquivalenz von normierten Basic Parallel Processes
  Christian Kuka   (Mai 2008)
   
• Graphische Benutzeroberfläche für HyKeY [pdf]
  Henning Rohlfs   (Februar 2008)
   
• XMI-Import und -Export für Syspect [pdf]
  Dominik Denker   (Juli 2007)
   
• Natürliches Schließen für den Shape Calculus [pdf]
  Sven Linker   (April 2007)
   
• MoDiShCa - Model Checking Discrete Shape Calculus [pdf]
  Jan-David Quesel   (Sep. 2005)
   
• Alternatives Backend für Jassda [pdf]
  Johannes Rieken   (Juni 2005)
   
• Entwicklung und Implementierung von Heuristiken zur optimierten Fehlersuche für PLC-Automaten [pdf]
  Nico Mischok   (Mai 2005)
   
• Anbindung einer Java-Implementierung an eine 3D-Animation [pdf]
  Andreea Taifas   (Feb. 2005)
   
• Entwicklung eines Javatools zur Übersetzung von Fehlerbäumen mit DC Semantik in Phasenautomaten [pdf]
  Casjen Schnars   (Nov. 2004)
   
• Temporallogische Spezifikation und CSP [ps]
  Andreas Schäfer   (Okt. 2000)
   
• Nicht-Implementierung von MIXGraphen unter PLGraph
  Martin Friedrich   (Jun. 2000)
   
• Fallstudie: Entwurf und Verifikation einer Zentralverriegelungssteuerung im KFZ mittels SPS-Automaten
  Marc Lettrari   (Jul. 1999)
   
• Z-Simulationstechniken als Grundlage für CSP-OZ-Simulation
  Bernd Westphal   (Jun. 1999)
   
• Ein Modelchecker für den Sequentiellen Duration Kalkül
  Holger Rasch   (Mai 1999)
   
• Untersuchung von HOL-Z anhand einer Fallstudie
  Boris Wirtz   (Feb. 1999)