Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Your Thesis

Topics for a Master thesis are in most cases related to recent research. If you interested in writing a thesis in our research group, please consult the list of open topics below or contact us directly. Further below you find a list of finished theses.

Bachelor Thesis Topics

Testoptimierung von Inter-Method Contracs in Java mit JMCTest
Advisor Abstract
Jan Haltermann

Motivation:
Im Jahr 2018 haben Boerding et al. das neue Konzept der Inter-Method Contracts für Java vorgeschlagen, welches das präzise Ausdrücken von Abhängigkeiten zwischen Methoden ermöglicht [1]. Sie stellten mit JMC eine Sprache zum Spezifizieren und mit JMCTest ein Tool zum dynamischen überprüfen der Inter-Method-Contracts von Javaprogrammen vor. JMCTest generiert vollkommen automatisch Objekte, auf denen die Methoden ausgeführt werden und die Validität der Contracts überprüft wird. Mit JMCTest konnten sie die Verletzung von Standard Inter-Method-Contracts in großen Projekten (z.B. JBoss, Java RT) nachweisen. Im Vergleich mit anderen Verifikationstools, die (manche) Inter-Method-Contracts prüfen, konnten Bugs gefunden werden, die von den anderen Tools nicht gefunden wurden.Obwohl JMCTest Contract-Verletzungen gefunden hat, ist es momentan noch ein akademischer Prototyp. Deshalb lässt sich das Tool an mehreren Stellen optimieren: Neben der Erweiterung des Funktionsumfangs, sodass z.B. Generics und innere Klassen unterstützt werden, kann der Algorithmus zur Erstellung und Modifikation der Eingaben der Test-Engine optimiert werden.

Ziele & Inhalt der Arbeit:
Ziel der Arbeit ist die Optimierung der Performance von JMCTest, um weitere Contract-Verletzungen zu finden. Deshalb sollen weitere Java-Features unterstützt werden. Das Tool soll in der Lage sein, Klassen zu analysieren, die Generics und innere Klassen enthalten und solche, die nicht über einen öffentlichen Konstruktor verfügen (z.B. mit dem Factory-Pattern). Darüber hinaus soll das Set der Elemente, die zur Generierung von Testdaten verwendet werden, erweitert werden. Momentan werden lediglich primitive Datentypen und Objekte zur Erstellung von Testdaten verwendet. Daher sollen komplexere Java-Konstrukte wie Arrays, Listen Maps und Enumerations unterstützt werden.  Darüber hinaus soll mindestens eine Strategie zur Modifizierung von Testdaten ausgearbeitet und implementiert werden. Solch eine Strategie kann zum Beispiel das zufällige Aufrufen von Methoden enthalten. Um besseres Feedback zu den gefundenen Verletzungen zu bieten, soll der Export der der Testfälle, die die Verletzung enthalten, verbessert werden.
Im Anschluss sollen die entwickelten Techniken evaluiert werden und mit potenziell mit ähnlichen Tools verglichen werden. Im Vergleich soll gezeigt werden, dass die Erweiterungen zu besseren Resultaten (mehr gefunden Fehlern) führen.Neben dem Contract „EqualsImpliesHashcode“ kann es noch weitere Contracts geben, die grundlegend in Java enthalten sind, z.B. für Datenstrukturen wie Arrays oder Listen. Wenn im Rahmen der Arbeite weitere Contracts identifiziert werden, soll die Performance von JMCTest mit ähnlichen Tools verglichen werden.

Literatur:
[1] Börding P., Haltermann J., Jakobs MC., Wehrheim H. (2018) JMCTest: Automatically Testing Inter-Method Contracts in Java. In: Medina-Bulo I., Merayo M., Hierons R. (eds) Testing Software and Systems. ICTSS 2018. Lecture Notes in Computer Science, vol 11146. Springer, Cham

Generierung von Programm-Invarianten mit Maschine Learning
Advisor Abstract
Jan Haltermann

Motivation:
Um die Korrektheit von Software zu analysieren, ist das Generieren von starken Invarianten eine entscheidende Aufgabe. Eine starke Invariante wird oftmals als Witness im Beweis der Korrektheit von Software verwendet. Daher ist dieser Bereich aktuell in der Forschung relvant. Im Jahr 2018 haben Zhu et al. einen Ansatz zum Lernen von Invarianten für Programme mit Schleifen entwickelt [1]. Zuerst werden dafür Testdaten generiert. Hierfür werden mögliche Werte der Schleifenvariablen während der Programmausführung generiert und klassifiziert, ob die Werte während einer Programausführung beobachtbar sind. Dafür wurden Constrained Horn Clauses verwendet. Im Anschluss wurde eine Support Vector Maschine (SVM) auf den generierten Daten trainiert. Das von der SVM gelernt Model stellt eine mögliche Programminvariante dar, die mit Hilfe von Decision Trees vereinfacht wurde.

Ziele und Umfang:
Während der Arbeit soll die vorgestellte Idee mit einem anderen ML Ansatz evaluiert werden. Dafür muss der Ansatz zuerst implementiert werden, wobei decision trees zum lernen von Invarianten verwendet werden sollen. Anstelle von Constrained Horn Clauses sollen zur Datengenerierung und zum Erzeugen von überapproximativen Gegenbeispielen Symbolic Execution verwendet werden. Diese Gegenbeispiele werden analysiert, um Testdaten zu generieren. Anschließend soll der neu entwickelte Approach mit dem ursprünglichen verglichen werden. Außerdem muss evaluiert werden, ob das Ersetzten der SVM durch anderen Verfahren (wie logistic regression) im Originalansatz zu besseren Resultaten führt. Die Implenentierung soll im CPAchecker [2] Framework erfolgen, wobei existierenden ML Bibliotheken verwendet werden sollen.

Literatur:
[1] Zhu, He, Stephen Magill, and Suresh Jagannathan. "A data-driven CHC solver." ACM SIGPLAN Notices. Vol. 53. No. 4. ACM, 2018.
[2] cpachecker.sosy-lab.org

Master Thesis Topics

Currently there are no master thesis topics available online

Feel free to contact us to probably get an individual topic: People

List of Finished Theses

Due privacy reasons full names of students will not be displayed.

Title Art
Aktualisierung von Android Apps mittels Soot Bachelor's Thesis
Neural Algorithm Selection for Software Verification Master's Thesis
Analyzing Data Usage in Array Programs Master's Thesis
Verification of Conflict Opacity for Software Transactional Memory Algorithms with Uppaal Master's Thesis
Combining Android Apps for analysis purposes Master's Thesis
Entwicklung einer statischen quantitativen Informationsflussanalyse Bachelor's Thesis
Korrektheitsbeweise für Muster von Servicekompositionen Bachelor's Thesis
Testing Java Method Contracts Master's Thesis
Evolutionäre Strategieberechnung für Timed Game Automata Bachelor's Thesis
Testing Opacity of Software Transactional Memory Algorithms Bachelor's Thesis
Cooperative static analysis of Android applications Master's Thesis
Korrektheitsüberprüfung von Invariantenkandidaten für nebenläufige Datenstrukturen Bachelor's Thesis
Verifikation von Opacity des Software Transactional Memory Algorithmus FastLane Master's Thesis
Verifikation von Service-Kompositionen mit Spin Bachelor's Thesis
Verifikation von Service-Kompositionen mit Prolog Bachelor's Thesis
Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung Bachelor's Thesis
Predicting Rankings of Software Verficaton Tools Using Kernels for Structured Data Master's Thesis
Program slicing: A Way of Separating C Program into Approximate and Precise Portions Master's Thesis
Evaluierung von Prozessmanagementlösungen im Hinblick auf agile Prozesse Bachelor's Thesis
Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs" Bachelor's Thesis
Ein hierarchischer Ansatz für temporale Planung bei erforderlicher Nebenläufigkeit Bachelor's Thesis
Generierung von Eigenschaften in einem Hardware/Software-Co-Verifikationsverfahren Bachelor's Thesis
Entwicklung eines Konzeptes zur Kodierung eines objekt-orientierten Typsystems in SMT Bachelor's Thesis
Visualisierung von SMT-Solver Ausgaben Bachelor's Thesis
Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB Master's Thesis
Linearisierbarkeitsbeweis der Work-Stealing Deque Bachelor's Thesis
Integration von History-basierten Korrektheits-Checks im Model Checker SPIN Bachelor's Thesis
Formal Semantics of Probalistic SMT Solving in Verification of Service Compositions Master's Thesis
Transformation graphischer Protokollspezifikationenin Model-Checker-Anfragen Bachelor's Thesis
Vergleichsstudie zur Ausdrucksstärke von SMT-Solvern Bachelor's Thesis
Analyse von Benutzeranforderungenan an Service-Kompositionen mittels Modelchecking Bachelor's Thesis
Berechnung von Memory Model-spezifischen Kontrollflussgraphen Bachelor's Thesis
Combining Three Valued Logic and Quantified Boolean Formulae in Bounded Model Checking Encodings Master's Thesis
Dreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von Gegenbeispielen Bachelor's Thesis
Suchraumeinschränkung für Graphgrammatiken druch tempoallogische Formeln Bachelor's Thesis
Multiagenten-Koordination in temporaler Planung Master's Thesis
Exploiting Planning Graphs and Landmarks for Efficient GTS Planning Master's Thesis
Bounded Model Checking für Graphtransformationssysteme als SAT-Problem Master's Thesis
Change and Validity Analysis in Deductive Program Verification Master's Thesis
Konzeption und Anwendung von Verhaltensmodellen in georeferenzierten Monitoringszenarien Bachelor's Thesis
Function Specification Inference Using Craig Interpolation Master's Thesis
Heuristic Search-Based Planning for Graph Transformations Systems Diplomarbeit
Reputation-based reliability prediction of service compositions Master's Thesis
Generierung von Shape-Analysen aus Graph-Spezifikationen Master's Thesis
Increasing the preciseness of shape analysis for graph transformations systems Master's Thesis
Modellierung und Analyse eines Bluetooth Protokolls mit Graphtransformationssystemen Bachelor's Thesis
Effiziente Validierung und Bewertung von Modellzerlegungen Diplomarbeit
Rückführung und Visualisierung von Gegenbeispielen aus einem Model Checker Bachelor's Thesis
Sichere Konfigurationsplanung adaptiver Systeme durch Model Checking Diplomarbeit
Bounded Model Checking für partielle Systeme Master's Thesis
Spezifikation des partiell replizierten, verteilten Systems DORS mit CSP-OZ in einem iterativen Entwicklungsprozess Diplomarbeit
Konzeption und Implementierung der Diagnose-Therapie-Komponente eines Softwarequalitätszykluses Bachelor's Thesis
Konzeption & Implementierung eines Dekompositions-Werkzeugs für kompositionelle Verifikation Diplomarbeit
Konzeption und Implementierung eines Testframeworks für parametrisierte Tests und Isolation des Testgegenstandes Diplomarbeit
Optimierung und Erweiterung einer Testsuite für eine Beschaffungslösung im öffentlichen Sektor Studienarbeit(DP04)
Automatisiertes kompositionelles Model Checking von CSP Spezifikationen Bachelor's Thesis
Variablenordnungsstrategien für den symbolischen Modelchecker TINY Studienarbeit(DP04)
Semantikerhaltende Transformation objekt-orientierter in zustandsbasierte Spezifikationen / Übersetzung von CSP-OZ nach ProZ Studienarbeit(DP04)
Entwurfsmuster in integrierten Methoden am Beispiel Object-Z Studienarbeit(DP04)
Evaluating a model checker for the analysis of refactorings Bachelor's Thesis
Erstellung einer CSP-OZ Spezifikation der Flugkontrolle eines Flughafens mittels Syspect Studienarbeit(DP04)
Grundlagen für Bounded Model Checking mit 3-wertiger Logik Studienarbeit(DP04)
Modellierung und Verifikation verteilter Systeme mit TINY Diplomarbeit
Verifikation von CSP-OZ mit SPIN Studienarbeit(DP04)
Design Pattern for Object-Z specifications Studienarbeit(DP04)
Entwicklung eines Übersetzers einer Teilsprache von CSP-OZ in die Eingabesprache CSPM von FDR2 Studienarbeit (DPO4)
Qualitätssicherung durch Optimierung des Testprozesses Studienarbeit(DPO4)
Generierung von Refaktoringwerkzeugen Master's Thesis

The University for the Information Society