Aufgabenstellung im Rahmen eines Interdisziplinären Projekts
Zertifizierte Implementierung von Algorithmen aus der Computeralgebra 

Diese Aufgabenstellung richtet sich an Studierende der Informatik, die ein Interdisziplinäres Projekt im Bereich Computeralgebra machen möchten. Ein solches Projekt kann die Nebenfachprüfung in der DHP ersparen!

Algebraische Algorithmen werden in der Kryptologie eingesetzt und kommen in vielen Applikationen vor, die eine geschützte Übertragung von Daten über das Internet sicher stellen sollen.  Ist die Implementierung dieser Algorithmen korrekt?  Wahrscheinlich schon.  Aber um sicher zu gehen, dass der Programmierer keinen schlechten Tag hatte, kann die Implementierung durch einen Korrektheitsbeweis zertifiziert werden.  Dies geschieht in einem sogenannten Theorembeweiser, in diesem Projekt in dem an der TU München entwickelten Isabelle-System.

Ziel dieses Projekts ist eine zertifizierte Implementierung des Algorithmus von Berlekamp zur Faktorisierung von Polynomen über endlichen Körpern.  Konkret wird in drei Schritten vorgegangen:

Das Ergebnis ist eine Implementierung des Algorithmus, die nicht nur die irreduziblen Faktoren des Eingabepolynoms liefert, sondern auch einen Beweis dafür, dass die Faktoren tatsächlich unzerlegbar sind.

Gegebenenfalls besteht die Möglichkeit, sich während der ersten beiden Schritte in Isabelle einzuarbeiten (d.h., falls Sie nicht zufällig schon das Isabelle-Praktikum besucht haben).  Der Schwerpunkt der Arbeit wird im dritten Schritt liegen.

Betreuer:
Dr. Clemens Ballarin, Tel. 289-17326, Raum FMI 01.11.061
Dr. Michael Kaplan, Tel. 289-17064, Raum FMI 02.12.035
Weitere Projekte für Studenten in der Isabelle-Gruppe.
Copyright © 2004 by Clemens Ballarin
Last updated 18 August 2004