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

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
Korrektheitsbeweise für Muster von ServicekompositionenBachelorarbeit
Testing Java Method ContractsMasterarbeit
Evolutionäre Strategieberechnung für Timed Game AutomataBachelorarbeit
Testing Opacity of Software Transactional Memory AlgorithmsBachelorarbeit
Cooperative static analysis of Android applicationsMasterarbeit
Korrektheitsüberprüfung von Invariantenkandidaten für nebenläufige DatenstrukturenBachelorarbeit
Verifikation von Opacity des Software Transactional Memory Algorithmus FastLaneMasterarbeit
Verifikation von Service-Kompositionen mit SpinBachelorarbeit
Verifikation von Service-Kompositionen mit PrologBachelorarbeit
Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer SoftwarezertifizierungBachelorarbeit
Predicting Rankings of Software Verficaton Tools Using Kernels for Structured DataMasterarbeit
Program slicing: A Way of Separating C Program into Approximate and Precise PortionsMasterarbeit
Evaluierung von Prozessmanagementlösungen im Hinblick auf agile ProzesseBachelorarbeit
Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs"Bachelorarbeit
Ein hierarchischer Ansatz für temporale Planung bei erforderlicher NebenläufigkeitBachelorarbeit
Generierung von Eigenschaften in einem Hardware/Software-Co-VerifikationsverfahrenBachelorarbeit
Entwicklung eines Konzeptes zur Kodierung eines objekt-orientierten Typsystems in SMTBachelorarbeit
Visualisierung von SMT-Solver AusgabenBachelorarbeit
Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIBMasterarbeit
Linearisierbarkeitsbeweis der Work-Stealing DequeBachelorarbeit
Integration von History-basierten Korrektheits-Checks im Model Checker SPINBachelorarbeit
Formal Semantics of Probalistic SMT Solving in Verification of Service CompositionsMasterarbeit
Transformation graphischer Protokollspezifikationenin Model-Checker-AnfragenBachelorarbeit
Vergleichsstudie zur Ausdrucksstärke von SMT-SolvernBachelorarbeit
Analyse von Benutzeranforderungenan an Service-Kompositionen mittels Modelchecking Bachelorarbeit
Berechnung von Memory Model-spezifischen KontrollflussgraphenBachelorarbeit
Combining Three Valued Logic and Quantified Boolean Formulae in Bounded Model Checking EncodingsMasterarbeit
Dreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von GegenbeispielenBachelorarbeit
Suchraumeinschränkung für Graphgrammatiken druch tempoallogische FormelnBachelorarbeit
Multiagenten-Koordination in temporaler PlanungMasterarbeit
Exploiting Planning Graphs and Landmarks for Efficient GTS PlanningMasterarbeit
Bounded Model Checking für Graphtransformationssysteme als SAT-ProblemMasterarbeit
Change and Validity Analysis in Deductive Program VerificationMasterarbeit
Konzeption und Anwendung von Verhaltensmodellen in georeferenzierten MonitoringszenarienBachelorarbeit
Function Specification Inference Using Craig InterpolationMasterarbeit
Heuristic Search-Based Planning for Graph Transformations SystemsDiplomarbeit
Reputation-based reliability prediction of service compositionsMasterarbeit
Generierung von Shape-Analysen aus Graph-SpezifikationenMasterarbeit
Increasing the preciseness of shape analysis for graph transformations systemsMasterarbeit
Modellierung und Analyse eines Bluetooth Protokolls mit GraphtransformationssystemenBachelorarbeit
Effiziente Validierung und Bewertung von ModellzerlegungenDiplomarbeit
Rückführung und Visualisierung von Gegenbeispielen aus einem Model CheckerBachelorarbeit
Sichere Konfigurationsplanung adaptiver Systeme durch Model CheckingDiplomarbeit
Bounded Model Checking für partielle SystemeMasterarbeit
Spezifikation des partiell replizierten, verteilten Systems DORS mit CSP-OZ in einem iterativen EntwicklungsprozessDiplomarbeit
Konzeption und Implementierung der Diagnose-Therapie-Komponente eines SoftwarequalitätszyklusesBachelorarbeit
Konzeption & Implementierung eines Dekompositions-Werkzeugs für kompositionelle VerifikationDiplomarbeit
Konzeption und Implementierung eines Testframeworks für parametrisierte Tests und Isolation des TestgegenstandesDiplomarbeit
Optimierung und Erweiterung einer Testsuite für eine Beschaffungslösung im öffentlichen SektorStudienarbeit(DP04)
Automatisiertes kompositionelles Model Checking von CSP SpezifikationenBachelorarbeit
Variablenordnungsstrategien für den symbolischen Modelchecker TINYStudienarbeit(DP04)
Semantikerhaltende Transformation objekt-orientierter in zustandsbasierte Spezifikationen / Übersetzung von CSP-OZ nach ProZStudienarbeit(DP04)
Entwurfsmuster in integrierten Methoden am Beispiel Object-ZStudienarbeit(DP04)
Evaluating a model checker for the analysis of refactoringsBachelorarbeit
Erstellung einer CSP-OZ Spezifikation der Flugkontrolle eines Flughafens mittels SyspectStudienarbeit(DP04)
Grundlagen für Bounded Model Checking mit 3-wertiger LogikStudienarbeit(DP04)
Modellierung und Verifikation verteilter Systeme mit TINYDiplomarbeit
Verifikation von CSP-OZ mit SPINStudienarbeit(DP04)
Design Pattern for Object-Z specificationsStudienarbeit(DP04)
Entwicklung eines Übersetzers einer Teilsprache von CSP-OZ in die Eingabesprache CSPM von FDR2Studienarbeit (DPO4)
Qualitätssicherung durch Optimierung des TestprozessesStudienarbeit(DPO4)
Generierung von RefaktoringwerkzeugenMasterarbeit

The University for the Information Society