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
- 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 |
---|---|
Optimierung von JMCTest beim Testen von Inter-Method Contracts | Bachelor's Thesis |
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 |