Navigation

Skiplinks

Kontakt

  • Leitung
    Prof. Dr. Ernst-Rüdiger Olderog
  • Sekretariat
    Andrea Göken
    Tel.: +49-(0)441-798-3121
    Fax.: +49-(0)441-798-2965
    E-Mail: Andreew7kaa./vstqGoekenus (Andrea.Goz/ekuxpaien@informatik.unigsi-oldenburg.x8q6dee2t)
    Raum: A3 2-208

Ausgeschriebene Arbeiten

Jede(r) Studierende muss, je nach Studiengang, eine Bachelor- oder Masterarbeit schreiben. Das ist selbstverständlich auch in unserer Abteilung möglich.

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

Abgeschlossene Bachelorarbeiten (Auswahl)

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

Abgeschlossene Masterarbeiten (Auswahl)

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

Abgeschlossene Studienarbeiten und Individuelle Projekte (Auswahl)

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

Abgeschlossene Diplomarbeiten (Auswahl)

  • Automatischer Beweis von Verifikationsbedingungen
    Reinhard Kluge   (April 2013)
     
  • Modellierung von Google Go im Pi-Kalkül
    Sören Jeserich   (Juli 2012)
  • Parallelität und Vererbung beim "Programmieren mit Vertrag"
    Detlef Bartetzko   (April 2012)
  • Algorithmen zum regulären Model-Checking
    Boris Rosenow   (Februar 2011)
     
  • Verifikationsarchitekturen in Syspect
    Matthias Peters   (August 2010)
     
  • Hiding Relaxed Semantics from a User:Design and Implementation of Fence Insertion Algorithms for Concurrent Programs
    Eike Möhlmann   (Juli 2010)
     
  • Experiment-based Analysis of PKCS#11
    Nils Sommer   (September 2009)
     
  • Model checking pi-Calculus against temporal connectedness properties [pdf]
    Sven Linker   (Dezember 2008)
     
  • Entwurf und Implementierung von Algorithmen zur Berechnung von Petrinetz-Semantiken für Pi-Kalkül-Prozesse [pdf]
    Tim Strazny   (Juli 2007)
     
  • Design By Contract for Java - Revised [pdf]
    Johannes Rieken   (April 2007)
     
  • Verifying Properties of Processes, Data, and Time: Linking Counterexamples to High-Level Specifications [pdf]
    Ulrich Hobelmann   (April 2007)
     
  • A Theorem Prover for Differential Dynamic Logic: Deductive Verification of Hybrid Systems [pdf]
    Jan David Quesel   (April 2007)
     
  • Integration von Verifikationswerkzeugen zur Systemanalyse mit Fehlerbäumen [pdf]
    Casjen Schnars   (Oktober 2006)
     
  • Integration von CSP-OZ in die OO-Softwareentwicklung für die automatische Verifikation [pdf]
    Andreea Stamer   (März 2006)
     
  • Runtime-Checking von JML-Spezifikationen mit Jass [pdf]
    Martin Schnaidt   (Feb. 2006)
     
  • SAT-based Verification for Abstraction Refinement [pdf]
    Stephanie Kemper   (Jan. 2006)
     
  • Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten [ps.gz] [pdf]
    Roland Meyer   (Aug. 2005)
     
  • Re-Design der MOBY-Klassenbibliothek in Java mit Implementierung eines graphischen Editors als Anwendungsbeispiel [pdf] [pdf]
    Andreas Schulze   (Feb. 2005)
     
  • Fehlerbaumverifikation durch Modelchecking mit Uppaal [pdf]
    Johannes Faber   (Mai 2004)
     
  • Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag [pdf]
    Mark Brörkens   (Jan. 2002)
     
  • Verifikation von Beweiskizzen mit Hilfe von SPIN
    Ingo Brückner   (Jan. 2002)
     
  • Fehlerbaumanalyse und Model-Checking [ps.gz]
    Andreas Schäfer   (Dez. 2001)
     
  • Eine Phasenautomatensemantik für SPS-Automaten
    Henning Tschirner   (März 2001)
     
  • Sicherheitsanalyse eines Protokolls zur Vertragsunterzeichnung
    Markus Wittwer   (März 2001)
     
  • Entwurf und Implementierung eines Algorithmus zur zeitlichen Analyse von Phasenautomaten
    Holger Rasch   (Sep. 2000)
     
  • Übersetzung von Phasenautomaten in Timed Automata
    Christian Mrugalla   (Jul. 2000)
     
  • Transforming CSP-OZ to Java assertions
    Thies Wellpott   (Jun. 2000)
     
  • Trace Zusicherungen in Jass - Erweiterung des Konzepts “Programmieren mit Vertrag”
    Michael Plath   (Jun. 2000)
     
  • Eine Testautomatensemantik für Constraint Diagrams und ihre Anwendung
    Marc Lettrari   (Apr. 2000)
     
  • Automatic conversion of the Formal Method CSP-OZ to FDR-CSP
    Boris Wirtz   (Mär. 2000)
     
  • Parsing, Typchecking und Transformation von CSP-OZ nach Jass
    Jens von Garrel   (Aug. 1999)
     
  • Hintergrundsimulation von SPS-Automaten [ps.gz]
    Michael Möller   (Jul. 1999)
     
  • Graphische Spezifikationssprachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams [ps.gz]
    Jochen Hoenicke   (Jun. 1999)
     
  • Parallelität und Vererbung beim “Programmieren mit Vertrag” - Weiterentwicklung von JaWA -
    Detlef Bartetzko   (Apr. 1999)
     
  • Implementierung von Constraint-Diagrammen
    Marco Oetken   (Okt. 1998)
     
  • Implementierung und Optimierung eines Modelcheckers für Trace-Logik
    Holger Bischoff   (Apr. 1998)
     
  • Graphische Spezifikationsformalismen
    Volker Grabowski   (Dez. 1997)
     
  • Sequentieller Duration Kalkül
    Arvid Hülsebus   (Okt. 1997)
     
  • “Programmieren mit Vertrag” in Java
    Dieter Meemken   (Sep. 1997)
     
  • Semantische Fundierung von CSP-Z
    Stefan Hallerstede   (Jan. 1997)
Wejkbmas1nter (mark.ketf0xtner1@uol.dexnjc) (Stand: 29.11.2018)