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.

Show image information

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
Marie-Christine JakobsPrograms-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.
Überführung von Pthread-Konzepten nach Promela für eine automatisierte Programverifikation
AdvisorAbstract
Oleg TravkinNebenläufige Programme nutzen oft Bibliotheken, wie z.B. Pthreads. Solche Bibliotheken implementieren Mechanismen zur Synchronisation, oder auch zur Erzeugung oder Zusammenführung von verschiedenen Prozessen. Bei der Verifikation von nebenläufigen Programmen müssen solche Mechanismen natürlich berücksichtigt werden. Gleichzeitig möchte man einen hohen Grad an Automatisierung erreichen. Das bedeutet, dass Korrektheitsbedingungen oftmals bereits im Programmcode vorhanden sind, z.B. in Form von Assertions, und das Programm nur noch ausgeführt oder dessen Zustandsraum exploriert werden muss (Model Checking).   Wegen des State-Explosion-Problems ist es aber ungeschickt, die Implementierung solcher Bibliotheken immer wieder zusammen mit dem eigentlichen Programm zu verifizieren. In der Verifikation verwendete Sprachen zur Modellierung von Programmverhalten, wie z.B. Promela, enthalten bereits identische oder ähnliche Konstrukte und können statt der Bibliotheks-Implementierung verwendet werden. An unserem Lehrstuhl wurde bereits ein Transformationsansatz entwickelt, der aus C Programmen (über einen Umweg über LLVM und Kontrollflussgraphen)  Promela Modelle generiert. Im Rahmen dieser Arbeit soll das Ersetzen von Bibliotheksaufrufen durch entsprechende Konstrukte der Sprache Promela konzipiert werden. Der bereits gegebene Transformationsansatz soll anschließend um die erarbeiteten Konzepte erweitert werden, so dass letztendlich Assertions in einem nebenläufigen Programm vollständig automatisiert geprüft werden können. Für die Evaluierung der Erweiterung sollen Fallstudien der Software Verification Competion (SV-Comp) herangezogen werden.

Master Thesis Topics

CPC+Test: A sequential combination of certificate validation and testing
AdvisorAbstract
Marie-Christine JakobsIn 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

Title NameArt
Testing Opacity of Software Transactional Memory AlgorithmsStefan MüssemeierBachelorarbeit
Cooperative static analysis of Android applicationsFelix PauckMasterarbeit
Korrektheitsüberprüfung von Invariantenkandidaten für nebenläufige DatenstrukturenSven HartwigBachelorarbeit
Verifikation von Opacity des Software Transactional Memory Algorithmus FastLaneMonika WedelMasterarbeit
Verifikation von Service-Kompositionen mit SpinDewender, Markus RudolfBachelorarbeit
Verifikation von Service-Kompositionen mit PrologHeinisch, PhilippBachelorarbeit
Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer SoftwarezertifizierungBröcher, HenrikBachelorarbeit
Predicting Rankings of Software Verficaton Tools Using Kernels for Structured DataCzech, MikeMasterarbeit
Program slicing: A Way of Separating C Program into Approximate and Precise PortionsZhang, GuangliMasterarbeit
Evaluierung von Prozessmanagementlösungen im Hinblick auf agile ProzesseBödefeld, JanBachelorarbeit
Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs"Korth, PhilippBachelorarbeit
Ein hierarchischer Ansatz für temporale Planung bei erforderlicher NebenläufigkeitHeil, JohannesBachelorarbeit
Generierung von Eigenschaften in einem Hardware/Software-Co-VerifikationsverfahrenPauck, FelixBachelorarbeit
Entwicklung eines Konzeptes zur Kodierung eines objekt-orientierten Typsystems in SMTKrakau, AndreasBachelorarbeit
Visualisierung von SMT-Solver AusgabenOsterbrink, SebastianBachelorarbeit
Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIBTöws, ManuelMasterarbeit
Linearisierbarkeitsbeweis der Work-Stealing DequeWedel, MonikaBachelorarbeit
Integration von History-basierten Korrektheits-Checks im Model Checker SPINDridger, KatharinaBachelorarbeit
Formal Semantics of Probalistic SMT Solving in Verification of Service CompositionsSanati, MaryamMasterarbeit
Transformation graphischer Protokollspezifikationenin Model-Checker-AnfragenKlauke, ChristophBachelorarbeit
Vergleichsstudie zur Ausdrucksstärke von SMT-SolvernEngelbrecht, MarcoBachelorarbeit
Analyse von Benutzeranforderungenan an Service-Kompositionen mittels Modelchecking Nickel, TobiasBachelorarbeit
Berechnung von Memory Model-spezifischen KontrollflussgraphenFeldmann, MichaelBachelorarbeit
Combining Three Valued Logic and Quantified Boolean Formulae in Bounded Model Checking EncodingsIkonomakis, NikolaosMasterarbeit
Dreiwertiges Model Checking paralleler Systeme mit heuristisch geleiteter Generierung von GegenbeispielenCzech, MikeBachelorarbeit
Suchraumeinschränkung für Graphgrammatiken druch tempoallogische FormelnFriedrich, MarcelBachelorarbeit
Multiagenten-Koordination in temporaler PlanungHauck, ThomasMasterarbeit
Exploiting Planning Graphs and Landmarks for Efficient GTS PlanningAhmadian, ShayanMasterarbeit
Bounded Model Checking für Graphtransformationssysteme als SAT-ProblemIsenberg, TobiasMasterarbeit
Change and Validity Analysis in Deductive Program VerificationJakobs, Marie-ChristineMasterarbeit
Konzeption und Anwendung von Verhaltensmodellen in georeferenzierten MonitoringszenarienBackhaus, PatrickBachelorarbeit
Function Specification Inference Using Craig InterpolationSchremmer, AlexanderMasterarbeit
Heuristic Search-Based Planning for Graph Transformations SystemsEstler, Hans-ChristianDiplomarbeit
Reputation-based reliability prediction of service compositionsBesova, GalinaMasterarbeit
Generierung von Shape-Analysen aus Graph-SpezifikationenBuckler, ChristophMasterarbeit
Increasing the preciseness of shape analysis for graph transformations systemsWonisch, DanielMasterarbeit
Modellierung und Analyse eines Bluetooth Protokolls mit GraphtransformationssystemenRizzi, MarcoBachelorarbeit
Effiziente Validierung und Bewertung von ModellzerlegungenPiepmeyer, MeikDiplomarbeit
Rückführung und Visualisierung von Gegenbeispielen aus einem Model CheckerMicus, SebastianBachelorarbeit
Sichere Konfigurationsplanung adaptiver Systeme durch Model CheckingRöhs, MalteDiplomarbeit
Bounded Model Checking für partielle SystemeTimm, NilsMasterarbeit
Spezifikation des partiell replizierten, verteilten Systems DORS mit CSP-OZ in einem iterativen EntwicklungsprozessBraun, RudolfDiplomarbeit
Konzeption und Implementierung der Diagnose-Therapie-Komponente eines SoftwarequalitätszyklusesBeister, FredericBachelorarbeit
Konzeption & Implementierung eines Dekompositions-Werkzeugs für kompositionelle VerifikationHerbold, KlausDiplomarbeit
Konzeption und Implementierung eines Testframeworks für parametrisierte Tests und Isolation des TestgegenstandesSchröder, MarinaDiplomarbeit
Optimierung und Erweiterung einer Testsuite für eine Beschaffungslösung im öffentlichen SektorDertmann, NadineStudienarbeit(DP04)
Automatisiertes kompositionelles Model Checking von CSP SpezifikationenWonisch, DanielBachelorarbeit
Variablenordnungsstrategien für den symbolischen Modelchecker TINYSteenken, DominikStudienarbeit(DP04)
Semantikerhaltende Transformation objekt-orientierter in zustandsbasierte Spezifikationen / Übersetzung von CSP-OZ nach ProZMüller, StevenStudienarbeit(DP04)
Entwurfsmuster in integrierten Methoden am Beispiel Object-ZXianghua, ZhengStudienarbeit(DP04)
Evaluating a model checker for the analysis of refactoringsEstler, Hans-ChristianBachelorarbeit
Erstellung einer CSP-OZ Spezifikation der Flugkontrolle eines Flughafens mittels SyspectJakoblew, MarcelStudienarbeit(DP04)
Grundlagen für Bounded Model Checking mit 3-wertiger LogikLiao, HaiStudienarbeit(DP04)
Modellierung und Verifikation verteilter Systeme mit TINYWalther, SvenDiplomarbeit
Verifikation von CSP-OZ mit SPINZorlu, FaithStudienarbeit(DP04)
Design Pattern for Object-Z specificationsYang, LeStudienarbeit(DP04)
Entwicklung eines Übersetzers einer Teilsprache von CSP-OZ in die Eingabesprache CSPM von FDR2Wagner, ElenaStudienarbeit (DPO4)
Qualitätssicherung durch Optimierung des TestprozessesMichalek, DominikaStudienarbeit(DPO4)
Generierung von RefaktoringwerkzeugenZiegert, SteffenMasterarbeit

The University for the Information Society