Abschlussarbeiten
Kontakt
Leitung
Sekretariat
Abschlussarbeiten
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)