Vorlesungsbegleitendes Forschungspraktikum
im Sommersemester 2022

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich, 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.

• Benutzerfreundliche Darstellung von Beweisverpflichtungen in DIVE

  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 dargestellt 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 zu der Frage, welche Darstellungsart von Benutzenden bevorzugt wird, gestaltet werden können.

  Betreuung: Wolfram Pfeifer, Mattias Ulbrich

• Modellierung und Verifikation eines Smart Contracts für ein Casino-Szenario

  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 soll ein bereits existierender Smart Contract als abstrakte Maschine in Event-B modelliert werden. 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

• Automatisches Finden von Wahlmanipulationen mittels Bounded Model Checking

  Die strategische Manipulation eines Wahlverfahrens ist die Abgabe einer Stimme, die von der eigenen Präferenz abweicht, mit dem Ziel, das Wahlergebnis stärker (als die "wirklich" präferierte Stimme) hin zur eigenen Präferenz zu beeinflussen. Es gibt ein grundsätzliches Ergebnis, dass jedes nicht-diktatorische Wahlverfahren mit mindestens drei Alternativen für solche Manipulationen anfällig ist. Manche Wahlverfahren lassen sich jedoch einfacher manipulieren als andere. Traditionell wird diese Fragestellung komplexitätstheoretisch untersucht, in neueren Arbeiten aber auch konkret quantifiziert.

  Das Projekt beinhaltet die Einarbeitung in obige Fragestellung, die Formalisierung einer solchen Quantifizierung für einfache Scoring-Wahlverfahren (z. B. relative Mehrheitswahl, Borda, ...) und die Entwicklung und Evaluation einfacher Experimente für den Bounded Model Checker CBMC, um solche Manipulationen für ein Wahlverfahren automatisch zu generieren und bewerten zu können.

  Betreuung: Michael Kirsten

• Formale Spezifikation und Verifikation verschiedener algorithmischer Fairnessbegriffe

  Unter einer ungerechtfertigten Diskriminierung eines Algorithmus versteht man, dass sich der Algorithmus für bestimmte Agenten anders verhält als für andere Agenten, obwohl es keine (akzeptierte) Rechtfertigung für diese Unterscheidung gibt. Ein Algorithmus, der nicht ungerechtfertigt diskriminiert, wird als fair bezeichnet. Allerdings existieren viele verschiedene solcher Diskriminierungs- bzw. Fairnessbegriffe, die auch in der Philosophie kontrovers diskutiert werden und bspw. für Fairness von Individuen und Fairness hinsichtlich Gruppenzugehörigkeit nicht immer miteinander vereinbar sind.

  Das Projekt beinhaltet die Einarbeitung in verschiedene Fairnessbegriffe, deren Formalisierung in einer Spezifikationssprache für ein Werkzeug zur formalen Verifikation von Software und das Schreiben einfacher zu verifizierender Beispielprogramme, sowie Experimente zur Verifikation der erstellten Programme. Hierbei soll mit einfachen Fairnessbegriffen angefangen und je nach Tauglichkeit der Spezifikationssprache auch zu "komplizierteren" Fairnessbegriffen übergegangen werden.

  Betreuung: Michael Kirsten, Lionel Blatter

• Quantifizierung von Fairness mittels Quantitativem Informationsfluss

  In diesem Projekt soll explorativ die Frage ergründet werden, ob die Entropiemaße des Quantitativen Informationsfluss (QIF) Rückschlüsse zur Fairness von Systemen geben können.

  QIF-Analysen erlauben, die Menge an geheimer Information zu bestimmen, die durch ein Programm oder System offenbart wird.

  Das Projekt beinhaltet die Einarbeitung in Thematik und Begrifflichkeiten von QIF-Analysen und deren Anwendung auf selbsterstellte (un-)faire Systeme.

  Betreuung: Alexander Weigl

• Ermittlung von Spezifikationsabdeckungen mittels Slicing

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

  In diesem Projekt soll diese Frage quantitativ angegangen werden. Die Zielsetzung besteht darin, zu bestimmen, wie viele (bzw. welche) Programmbefehle überhaupt einen Einfluss auf die Spezifikation haben. Hierzu soll eine Pipeline aus den folgenden bestehenden Werkzeugen gebaut werden: (a) eine spezifikationsgetriebene Generierung von Laufzeitbedingungen (sogenannte Runtime Assertions) sowie (b) ein Programm-Slicer.

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

  Betreuung: Alexander Weigl, Mattias Ulbrich

• Regression von Informationsfluss in Probabilistischen Programmen

  Vertraulichkeit ist ein wichtiges Schutzziel in der IT-Sicherheit. Auf Programmebene beweist man dafür, dass geheime Informationen keinen Einfluss auf öffentlich beobachtbare Ausgaben haben. In diesem Fall sagt man, das Programm hat kein Informationsleck. In der Softwareevolution ist man nun daran interessiert, dass die Menge der Informationslecks über die Softwareversionen nicht zunimmt; also dass keine Regression bei Informationlecks auftritt. In diesem Forschungspraktikum sollen solche Regressionen in probabilistischen Programmen formal erschlossen werden.

  Das Projekt beinhaltet die Einarbeitung in sicheren (secure) Informationfluss in probabilistischen Programmen, die Formalisierung der Regression von Informationslecks, sowie die Gestaltung, Durchführung und Interpretation der Experimente.

  Betreuung: Alexander Weigl, Mattias Ulbrich

Ansprechperson

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