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

Evaluation eines Programs-from-Proofs Ansatzes für Informationsflusskontrolle
Advisor Abstract
Manuel Töws Programs-from-Proofs ist ein Verfahren zur einfachen Sicherstellung von der Korrektheit von Software, die bei einem Nutzer ausgeführt wird. In dem Verfahren prüft der Hersteller einer Software aufwändig die Korrektheit bezüglich der gegebenen Anforderungen und nutzt anschließend den Beweis, um die Software in eine schneller prüfbare und dennoch verhaltensäquivalente Version zu transformieren. Bisher haben wir dieses Verfahren für Sicherheitseigenschaften wie Protokolle und Invarianten benutzt. In dieser Abschlussarbeit soll ein bereits theoretisch beschriebenes Verfahren [1] evaluiert werden, welches Security Eigenschaften mittels Typsystemen prüft. Konkret prüft das Verfahren, dass keine unerlaubten Informationsflüsse auftreten, z.B. eine Variable am Programmende keine Informationen über Anfangswerte von Variablen mit höherem Sicherheitslevel enthält. In der Abschlussarbeit sollen die Typprüfungsverfahren auf Seiten des Herstellers und Nutzers sowie die Programmtransformation implementiert werden. Anschließend soll praktisch evaluiert werden, wie viel besser (z.B. bzgl. Zeit und Speicherbedarf) die Prüfung des transformierten Programms gegenüber der Prüfung des originalen Programms beim Hersteller ist. Dafür müssen auch geeignete Programme(Benchmark) gefunden werden.
Literatur:
[1] Sebastian Hunt and David Sands. 2006. On flow-sensitive security types. In Symposium on Principles of Programming languages (POPL '06). ACM, 79-90. http://doi.acm.org/10.1145/1111037.1111045
[2] Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A sound type system for secure flow analysis. J. Comput. Secur. 4, 2-3 (January 1996), 167-187.
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

Master Thesis Topics

CPC+Test: A sequential combination of certificate validation and testing
AdvisorAbstract
Manuel Töws
In our previous work [1], we studied three approaches for a combination of verification and testing based on the concept of conditional model checking [2]. This master thesis should transfer the idea of combined verification and testing into the context of (configurable) program certification.  We assume that the code consumer does not have enough time to validate the whole certificate and only validates parts of the certificate. Thus, we only know for a part of the program that it is safe w.r.t. the property of interest. After such a partial certificate validation, the program parts which are not assured by the partial certificate validation should be tested.

The goal of the master thesis is to adapt the existing configurable program certification from [3] s.t. a partial certificate validation becomes feasible and the result of a partial certificate validation is summarized in a condition. The condition can then be used similar to our previous work [1] to construct the residual program for testing. It must be shown that the construction of the condition is sound, i.e., it only omits program paths whose safety is assured by the partial certificate validation.  Furthermore, the adaption should be implemented in and evaluated with the software analysis tool CPAchecker. At best, also strategies are developed considering how to arrange the certificate elements s.t. the residual program obtained after a partial certificate validation becomes small.

[1] Mike Czech, Marie-Christine Jakobs, Heike Wehrheim:  Just Test What You Cannot Verify! FASE 2015: pp. 100-114.
[2] Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, Philipp Wendler: Conditional model checking: a technique to pass information between verifiers. SIGSOFT FSE 2012.
[3] Marie-Christine Jakobs: Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning. SEFM 2015: pp. 159-174.

List of Finished Theses

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

Title Art
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