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
Klassifikation von Online-Verifikationsmerkmalen
Advisor Abstract
Cedric Richter Motivation:
Der automatisierten Softwareverifikation fehlt die menschliche Intuition, und das wollen wir ändern.
Die Softwareverifikation ist ein Forschungsgebiet, welches sich mit dem Beweis oder Widerleg der Korrektheit eines
Softwaresystems beschäftigt. 
Während der Verifikation erforschen viele Techniken den Zustandsraum eines Programms, um eine fehlerhafte Ausführung zu entdecken oder das System als korrekt zu verifizieren.
Im Fall eines fehlerhaften Programmes, neigen jedoch viele bestehende Techniken dazu, ihre Zeit mit der Erkundung korrekter
Teile des Programmes zu verschwenden. Eine Anpassung des Suchstrategie oder das Wechseln zu einem anderen Verifikationsalgorithm
könnte in diesen Fällen von Vorteil sein. 
Mit der Hilfe von maschinellem Lernen wollen wir ein Algorithmus entwerfen, der diese Situationen während der Verifikation erkennt und sich online an das jeweilige Problem anpasst.

Ziele & Inhalt der Arbeit:
Die Erfassung relevanter Daten und die Erstellung eines aussagekräftigen Datensatzes ist ein wesentlicher Bestandteil datengetriebener Algorithmen. Ziel dieser Arbeit ist daher die automatische Generierung eines Datensatzes zum Lernen von Verifkationsverhalten.
Zu diesem Zweck sollte eine Technik entwickelt und implementiert werden, die das Suchverhalten eines Verifikationsalgorithmus analysiert, relevante Ereignisse identifiziert und die gesammelten Informationen in einem geeigneten Format speichert.
Der entwickelte Ansatz soll dann in das Verifikationsframework CPAchecker [1] integriert werden, welches uns auch die
notwendigen Verifikationsalgorithmen liefert. Letztendlich soll die neuartige Technik zur Erzeugung eines Datensatzes eingesetzt werden, während die Performanz und Qualität des Generierungsprozesses evaluiert werden soll.
Es ist auch möglich, das Thema im Rahmen einer Masterarbeit zu bearbeiten. In diesem Fall ist die Datengenerierung nur der erste Teil. In einem zweiten Teil soll ein maschineller Lernalgorithmus entwickelt werden, der die Erfolgswahrscheinlichkeit der aktuellen Verifikation voraussagt. Der Lernalgorithmus soll dann in Bezug auf Accuracy und Laufzeit evaluiert werden.

Links: [1] cpachecker.sosy-lab.org
 
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

Classification of online features for verification
Advisor Abstract
Cedric Richter

Motivation:

Automated software verification lacks human intuition and we like to change this.
Software verification is a research field which focuses on proving or refuting the correctness of a software systems. During the process, virtually all techniques explore the state space of a program to find an erroneous execution or verify the system as correct. However, in the presence of a bug, many existing techniques tend to waste lot of time in exploring correct parts of the program, while switching the search strategy or the verification algorithm might be more beneficial. By applying machine learning, we aim for an algorithm that recognizes these situations during verification and adapts online to the problem at hand.


Goals:

Collecting relevant data and creating an informative dataset is a crucial part of data-driven algorithms. Hence, the goal of this thesis is the automatic generation of a dataset for learning from verification runs.  For this purpose, a technique should be developed and implemented that tracks the search behaviour of a verification strategy, identifies relevant events and stores the information in an appropriate format. Furthermore, the developed approach should be integrated in the verification framework CPAchecker [1], which provides us with the necessary verification strategies. However, data generation is only the first part. In a second part, a machine learning algorithm should be developed that predicts the success probability of the current verification run. The learning algorithm should then be evaluated in terms of prediction accuracy and runtime.

Links:

[1] cpachecker.sosy-lab.org

 

Refinement Testing of Java Collections
Advisor Abstract
Heike Wehrheim

Motivation:

Data refinement is an established design principle within formal methods. It aims at a hierarchical design of systems, where the data to be stored and the operations on this data are first of all specified on an abstract, formal level, and later refined into concrete implementations. The abstract specification serves as a correctness specification for the implementation. Thus implementations need to be checked (verified or tested) for correctness.


Goals:

The goal of this thesis is the development of a testing technique for refinement checking. It targets Java implementations of common data structures like sets, stacks or queues as are part of the Java Collections framework. The following tasks have to be performed:
  • definition of a machine readable language for abstract specification,
  • derivation of test goals for Collections classes out of abstract specifications(stated in terms of data refinement terminology: defining the abstraction relation and computing concretisations),
  • construction of test objects (i.e, Java objects) and
  • test execution.
The testing approach is to be evaluated on examples of the Java Collections framework.  

Links:

  • John Derrick, Eerke A. Boiten: Refinement in Z and Object-Z - Foundations and Advanced Applications (2. ed.). Springer 2014.
  • Gary Leavens, Yoonsik Cheon: Design by Contract with JML.
  • Paul Börding, Jan Haltermann, Marie-Christine Jakobs, Heike Wehrheim: JMCTest: Automatically Testing Inter-Method Contracts in Java. ICTSS 2018.
 

 

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