Themen für Diplomarbeiten, Masterarbeiten und Individualpraktika
Themenstellungen für Diplom-, Masterarbeiten und Praktika kommen überwiegend aus den Bereichen Requirements- und Software-Engineering, Übersetzerbau und Constraint-Programmierung. Grundlagen werden in den entsprechenden, regelmäßig angebotenen Lehrveranstaltungen des Institus vermittelt. Die Themen orientieren sich an unseren Forschungsgebieten. Darüberhinaus sind wir für eigene Vorschläge offen. Bei Interesse wenden Sie sich an die Dozenten des Instituts.
Die folgende, unvollständige Liste bietet eine Auswahl konkreter Themen und Themenbereiche. Genauere Informationen dazu erhalten Sie bei den jeweiligen Ansprechpersonen.
- Bounded reachability Analyse von Model Programs mit BoogiePL als Zwischensprache
Model Programs sind eine Teilmenge der Abstract State Machines (
http://www.eecs.umich.edu/gasm/). Dabei handelt es sich um eine formale Sprache die z.B. dazu verwendet wird, um Protokolle oder Programme zu spezifizieren und schließlich gemäß dieser Spezifikation zu verifizieren. Für diese Verifikation ist es notwendig, die Model Programs in eine Verifikationsbedingung zu überführen, die dann von einem (automatischen) Theorembeweiser bewiesen oder eben widerlegt werden kann.
Im Rahmen des Projekts Spec# (
http://research.microsoft.com/SpecSharp/) von Microsoft Research wurde zur Programmverifikation eine Zwischensprache namens BoogiePL entwickelt, die höhere Konstrukte bietet als die meisten aktuellen Theorembeweiser. Ziel dieser Arbeit ist es nun, Model Programs (oder zumindest bestimmte Teile davon) über BoogiePL in eine Verifikationsbedingung zu übersetzen, so dass deren Korrektheit (für eine beschränkte Anzahl von Schritten) bewiesen werden kann.
Kontakt:
Alexander Raschke - Eine Liste möglicher Themen von Prof. Frühwirth ist hier verzeichnet.
Kontakt: Thom Frühwirth - Verschiedene Praktika und Themen für Arbeiten im Bereich der Constraint-Programmierung und Constraint Handling Rules sind
hier aufgeführt.
