Proseminar SS2022

Zertifizierende Algorithmen

Inhalt

Algorithmen sind überall. Aber wo viel programmiert wird, gibt es auch Bugs. Während Bugs mit vielen Tests oft erkannt werden können, sind diese keine Garantie für Richtigkeit. Deshalb gibt es das Konzept der zertifizierenden Algorithmen:
Neben dem Resultat geben sie einen kurzen und simplen Beweis (Zertifikat) an, dass das Ergebnis richtig ist. Die Stärke dieses Verfahrens ist, dass der Benutzer selber überprüfen kann, ob die Ausgabe korrekt ist – und das schneller als dieses oder ein anderes Programm nochmal auszuführen oder gar das ganze Programm formal zu verifizieren. So ist kein Vertrauen in die Richtigkeit des Programmes nötig.

Um kurze Zertifikate zu ermöglichen, muss man oft hilfreiche Strukturen des Problems ausnutzen. Deshalb ist das Feld der Zertifizierenden Algorithmen so interessant, nicht nur weil sie nützlich sind, sondern auch tiefe Einblicke in ein Problem födern.

Es gibt für zertifizierende Algorithmen viele Beispiele: Um den größten gemeinsamen Nenner zu bestimmten, nutzt man den Euklidischen Algorithmus. Um zu überprüfen, ob das Ergebnis wirklich der größte gemeinsame Nenner ist, müsste man die Rechnung wiederholen. Ein zertifizerender Algorithmus ist der erweiterte Euklidische Algorithmus (bekannt aus DS).

Auch in der Graphentheorie gibt es viele Beispiele: von relativ einfach bis hin zu ganz ausgefuchst. Relativ simpel sind hier, die Zusammenhangskomponenten eines Graphen herauszufinden oder zu überprüfen, ob ein Graph bipartit ist. Ausgeklügelter ist da schon der zertifizierende Algorithmus für den Planaritätscheck, also zu überprüfen, ob ein Graph auf der Ebene ohne Kantenüberkreuzungen einbettbar ist.

Ort und Zeit

Das Proseminar findet semesterbegleitend wöchentlich statt.

Der erste Vortragstermin ist am 02.05., alle weiteren Termine sind der untenstehenden Tabelle zu entnehmen.

Die Teilnahme an diesem Proseminar ist nur nach einer Anmeldung im Supra moeglich!

Material

• Kickoff-Folien
• Template für Ausarbeitung
• How to Present a Paper: A Speaker’s Guide

Termine und Themen

Datum	Thema	Student*in
28.03.2022	Kickoff	Alle
31.03.2022	Themenvergabe	Alle
02.05.2022	Program result checking: A new approach to making programs more reliable	Firas M. / Felix B.
09.05.2022	Self-Testing/Correcting with Applications to Numerical Problems	Andrei M.
16.05.2022	A Framework for the Verification of Certifying Computation	Felix E.
23.05.2022	Checking the correctness of Memories	Cedric D. / Omar M.
30.05.2022	Linear-time certifying recognition algorithms and forbidden induced subgraphs	Hannah B.
13.06.2022	Checking Linked Data Structures	Elliot J.
20.06.2022	Reflections on the Pentium Division Bug	Simon H.
27.06.2022	Program Checkers for Probability Generation	Arthur B.
04.07.2022	Designing Checkers for Programs that Run in Parallel	Franklin Z.
11.07.2022	Spot-Checkers	Laura R.