Vorlesungsbegleitendes Forschungspraktikum

Prof. Dr. Bernhard Beckert, Michael Kirsten

Typ: Praktikum
Zielgruppe: Master Informatik
Umfang: 5 Leistungspunkte (3 Praktikum + 2 Schlüsselqualifikation)
Ort: nach Absprache

Inhalt

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen innerhalb der ersten Woche bewerben können (die Plätze sind begrenzt!). Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität der Forschungsgruppe und trägt zu deren Erfolg bei.

Beispiele für solche Forschungsaktivitäten sind etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums auf drei bis fünf Seiten dokumentiert, sowie zum letzten Vorlesungstermin im Rahmen eines Kolloquiums in jeweils etwa 10 bis 15 Minuten präsentiert und in einer anschließenden Fragerunde diskutiert.

Qualifikationsziele

  • Einen Forschungsansatz und die eigene Forschungs(teil-)aufgabe verstehen, begründen, bewerten und einordnen können
  • Aus der Aufgabenbeschreibung konkrete Arbeitsschritte entwickeln können
  • In dem Forschungsbereich des Projekts wissenschaftlich arbeiten können
  • Die für das Projekt relevanten inhaltlichen Grundlagen kennen, einsetzen und die Relevanz für die Fragestellung bewerten können
  • Forschungsergebnisse dokumentieren, zusammenfassen und präsentieren, sowie diskutieren können

Methodische Begleitveranstaltungen

Neben der Forschungsarbeit umfasst das Praktikum auch die folgenden mit der Projektarbeit verzahnten methodischen Veranstaltungen im Rahmen von zwei Leistungspunkten (LP), die im Rahmen des Forschungspraktikums als Schlüsselqualifikationsleistungen zu besuchen sind:

  • Literaturrechereche und Zitieren (2,0 Stunden)
  • Projektmanagementworkshop (7,0 Stunden)
  • Präsentationsworkshop (8,0 Stunden)
  • Erkenntnistheorie (1,5 Stunden)
  • Wissenschaftstheorie (1,5 Stunden)
  • Workshop zum Aufstellen einer Forschungsfrage (3,0 Stunden)
  • Schreiben von Forschungsanträgen (1,5 Stunden)
  • Experimentaldesign (1,5 Stunden)

Die Workshops zu Projektmanagement und Präsentationen finden in Kooperation mit dem House of Competence (HoC) statt. Alle Veranstaltungen sind gezielt auf Forschungsprojekte im Bereich der Informatik ausgerichtet. Die Termine der Veranstaltungen werden zu Vorlesungsbeginn bekanntgegeben.

Themen

Die Themen werden zu Beginn der Vorlesung vorgestellt. Zudem sind wir offen für Themenvorschläge, die im Zusammenhang zur Vorlesung bzw. zur Forschung unserer Forschungsgruppe stehen. Beispiele hierfür sind Forschungsaktivitäten wie etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation ausgewählter formaler Methoden (u.ä.). An dieser Stelle werden wir vor Beginn der Vorlesung eine Auswahl geplanter Themen auflisten. Bei Fragen hierzu können Sie sich bereits im Vorfeld bei den genannten Ansprechpersonen melden. Gern gesehen sind auch Initiativanfragen zu Themengebieten unserer Forschungsgruppe.

  • Zugängliche Darstellung von Beweisverpflichtungen für der Programmverifikation

    Bei der formalen Verifikation von Spezifikationen für Programme kann man im Allgemeinen nicht erwarten, dass diese Verifikation immer vollautomatisch ablaufen kann. Einerseits können sich Fehler in Programm oder Spezifikation eingeschlichen haben, andererseits können die automatischen Werkzeuge an ihre Grenzen stoßen.

    Um dennoch möglichst viele spezifizierte Programme verifizieren zu können, ist es wichtig, dass die Beweisverpflichtung, die hinter der Spezifikation steht, sehr zugänglich dargstellt wird und nach Möglichkeit auch Modifikation und Interaktion zulässt.

    Auf Grundlage des interaktiven Verifikationssystems DIVE soll in diesem Forschungspraktikum ein Visualisierungsprototyp für Beweisverpflichtungen entwickelt werden, mit dem Experimente gestaltet werden können, welche Darstellung von Benutzern bevorzugt wird.

    Betreuung: Wolfram Pfeifer, Mattias Ulbrich

  • Modellierung und Verifikation eines Smart Contracts

    Smart Contracts sind Programme, die bestimmte Funktionalitäten in einem dezentralen Netzwerk zur Verfügung stellen. Da sie oft den Zugang zu Währung oder anderen Ressourcen verwalten, ist es sehr wichtig, schon vor der Veröffentlichung des Programms zu überprüfen, ob es sich immer korrekt verhält. Zu diesem Zweck kann es sinnvoll sein, eine Smart-Contract-Anwendung auf einer abstrakteren Ebene zu modellieren, um dann beispielsweise Safety- und Livenesseigenschaften spezifizieren und beweisen zu können.

    In diesem Projekt sollen Sie einen bereits existierenden Smart Contract als abstrakte Maschine in Event-B modellieren. Dies beinhaltet eine Einarbeitung in Event-B und das Werkzeug Rodin. Weiterhin soll versucht werden, Safety- und Livenesseigenschaften des entstandenen Modells zu spezifizieren und verifizieren.

    Betreuung: Jonas Schiffl

  • Ermittlung von Spezifikationsabdeckungen mittels Slicing

    Die Validität einer formalen Spezifikation ist eine klassische Fragestellung formaler Methoden. Diese besteht in der Übersetzungen einer "gemeinten", "gedachten" und "erwarteten" (d.h. insbesondere informellen) Spezifikation in eine formale Spezifikation.

    In diesem Projekt gehen Sie diese Frage quantitativ an. Die Zielsetzung besteht darin, zu bestimmen, wie viele (bzw. welche) Programmbefehle überhaupt einen Einfluss auf die Spezifikation haben. Hierzu bauen Sie eine Pipeline aus den folgenden bestehenden Werkzeugen: (a) einer spezifikationsgetriebenen Generierung von Laufzeitbedingungen (sogenannten Runtime Assertions) sowie (b) einem Programm-Slicer.

    Das Projekt beinhaltet die Einarbeitung in die obige Fragestellung, die Formalisierung des Problems, sowie der Konstruktion der Pipeline und deren anschließender Evaluierung.

    Betreuung: Alexander Weigl, Mattias Ulbrich

  • Verifikation des "Verifying Key Servers" HAGRID

    Seit letztem Jahr ist HAGRID der neue Standard für PGP-Keyserver. Diese Neuentwicklung war notwendig, da der alte PGP-Keyserver aufgrund diverser Sicherheits- und Datenschutzvorfälle (CVE-2019-13050, GPRD), sowie Performanceproblemen nicht mehr tragfähig war.

    Aber verwaltet HAGRID die Schlüssel auch korrekt? Ist es sicher?

    HAGRID ist Gegenstand des diesjährigen Verifikationswettbewerbs "VerifyThis LongTerm Challenge".

    In diesen Projekt wenden Sie das Verifikationswerkzeug KeY an, um die Korrektheit einer abstrahierten, auf den kritischen Kern fokussierten Java-Version von HAGRID zu beweisen. Hierzu gibt es bereits erste Untersuchungen – allerdings mit der vereinfachenden Annahme, dass die gespeicherten E-Mails und öffentlichen Schlüssel nur Integer (und bspw. keine Strings) sind.

    An diese Untersuchung schließt sich dieses Projekt an: Wir wollen nun eine Version verifizieren, die mit Zeichenketten arbeitet. Neben der Verifikation kann dieses Projekt auch Erweiterungen der logischen Modellierung in KeY umfassen.

    Betreuung: Mattias Ulbrich, Alexander Weigl

Ansprechpartner

Bei Fragen rund um das Thema Forschungspraktikum (hier oder bei anderen Vorlesungen) können Sie sich bei Michael Kirsten melden.