Vorlesungsbegleitendes Forschungspraktikum
im Sommersemester 2025

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich, Dr. Michael Kirsten

Typ:	Praktikum
Zielgruppe:	Master Informatik
Umfang:	5 Leistungspunkte (3 Praktikum + 2 Schlüsselqualifikation)
Ort:	n.V.
Veranstaltungs-Nr.:	2400281

Zur Seite der Vorlesung

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.

• Large Language Models für die Synthese von JML-Spezifikationen aus Javadoc-Kommentaren

  Für die Programmverifikation von Java-Programmen braucht es formale Spezifikationen der zu untersuchenden Routinen. Für die Anwendung deduktiver Beweismethoden wie bspw. in KeY ist die geeignete Spezifizierung von Klasseninvarianten und von Verträgen für Methoden notwendig. Üblicherweise liegen die Beschreibungen der Funktionalität von Klassen aber lediglich in natürlicher Sprache in API-Beschreibungen z. B. in Javadoc-Kommentaren vor. Ziel dieses Praktikums ist es, die Möglichkeiten und Grenzen der Verwendung von LLMs wie ChatGPT für die Generierung von JML-Spezifikationen aus informellen Javadoc-Annotationen zu evaluieren.

  Betreuung: Samuel Teuber, N.N.

• Analyse von Langzeit-Fairness mittels Probabilistischem Model Checking

  Dieses Projekt befasst sich mit der Frage von Langzeit-Effekten im Kontext algorithmischer Fairness: D’Amour et al. [1] untersuchten hierzu bereits wie sich Fairness-Eigenschaften verhalten, wenn man den Feedback-Loop zwischen einer algorithmischen Entscheidung und gesellschaftlicher Dynamik über längere Zeiträume betrachtet und ergänzten hiermit die Arbeit von Liu et al. [2].

  Das Ziel des Projektes wäre es zunächst eine von D’Amour et al. präsentierte Fairness-Simulationen (bspw. zur Kreditvergabe) mithilfe eines probabilistischen Model Checkers (z. B. mit Storm [3]) nachzubauen und die Ergebnisse dort (soweit möglich) zu reproduzieren. Im Anschluss sollen die Modelle dann um weitere Effekte ergänzt werden, um zu analysieren inwieweit dies Fairness-Eigenschaften verändert.

  [1] D'Amour, Alexander, et al. "Fairness is not static: deeper understanding of long term fairness via simulation studies." Conference on Fairness, Accountability, and Transparency (FAT* 2020).
  [2] Liu, Lydia T., et al. "Delayed impact of fair machine learning." International Conference on Machine Learning (PMLR 2018).
  [3] Hensel, Christian, et al. "The probabilistic model checker Storm." International Journal on Software Tools for Technology Transfer 24.4 (2022): 589-610.

  Betreuung: Samuel Teuber, N.N.

• Erweiterung der Beispielsammlung von KeY

  Why3 ist ein deduktives Verifikationswerkzeug, das Ähnlichkeiten zu KeY besitzt, Anders als KeY arbeitet es auf einer abstrakteren Programmiersprache, die einfacher zu verifzieren ist als KeY. Aufgabe in dem Forschungspraktikum ist es, einige Beispiele aus der Sammlung Toccata für die Verifikation in KeY einzurichten. Insbesondere soll dabei beantwortet werden:

  • Welche Herausforderungen entstehen dadurch, dass KeY auf einer realen Programmiersprache arbeitet und nicht auf einer verifikationsfreundlichen Zwischensprache (IR)?
  • Welche Modellierungstechniken können von Why3 nach KeY gewinnbringend übertragen werden?

  Betreuung: Mattias Ulbrich, N.N.

• Erweiterung der Theorie endlicher Abbildungen in Isabelle/HOL

  Interaktive Theorembeweiser wie Isabelle/HOL ermöglichen es, formale Korrektheit von in ihnen formulierten Beweisen zu ermöglichen, indem automatisch jeder Schritt gegen den zugrunde liegenden Kalkül geprüft wird. In der Praxis heißt das aber auch, dass jedes im Beweis referenzierte Konzept bereits selbst ebenso formalisiert sein muss. Isabelle/HOL enthält dafür eine große Sammlung fertiger Theorien, die ähnlich einer Standard Library einer Programmiersprache einfach benutzt werden kann. Darin enthalten sind Theorien über Abbildungen (Map.thy: partielle Funktionen, die nicht notwendigerweise für jedes Argument einen Wert haben) sowie endliche Abbildungen (Finite_Map.thy: Abbildungen, die nur für endliche viele Argumente einen Wert liefern). Letztere ist allerdings wesentlich weniger umfangreich: viele oft hilfreiche Aussagen, die für allgemeine Abbildungen bereits existieren, fehlen für endliche Abbildungen. Ziel dieses Praktikums ist es, zu bestimmen, welche mit geringem Aufwand übertragen werden können, und diese entsprechend für endliche Abbildungen anzupassen.

  Betreuung: Terru Stübinger

Ansprechperson

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