Hauptseminar im Wintersemester 2003/4
Programmkorrektheit durch Ergebnisprüfung zur Laufzeit
Kontaktpersonen:
| Peter Rossmanith (rossmani@informatik.rwth-aachen.de) |
| Stefan Richter (richter@informatik.rwth-aachen.de) |
Einordnung
Theoretische InformatikOrt und Zeit
Dienstag 14:15 im Seminarraum 4013 (Informatik I)Inhalt
Ein program correctness checker ist ein Algorithmus, der das Ergebnis einer Berechnung überprüft. Gegeben sei eine Funktion f, die von einem Programm P berechnet werden soll, und eine Eingabe x. Ein checker für f ist dann eine probabilistische Turingmaschine, die mit hoher Wahrscheinlichkeit akzeptiert, wenn P korrekt ist, also P(y)=f(y) für alle y, und mit hoher Wahrscheinlichkeit verwirft, wenn P auf der speziellen Eingabe x nicht mit der Funktion f übereinstimmt.Solche Ergebnisprüfer haben zahlreiche Anwendungen beim Entwurf von Programmen. Das Seminar soll ausgehend von einer Einführung zunächst solche Methoden aufzeigen. Weitere Vorträge gehen auf einzelne algorithmische Techniken ein. Ergänzend sollen Zusammenhänge mit Entwicklungen in der Komplexitätstheorie dargestellt werden.
Voraussetzungen
Vordiplom. Vorkenntnisse in den Gebieten Algorithmen, Randomisierung und Komplexitätstheorie können hilfreich sein.Hinweise
- Vortrag: Die TeilnehmerInnen gestalten das Hauptseminar durch ihre Vorträge. Im Anschluß an jeden Vortrag besteht die Möglichkeit zu Fragen an den/die Vortragende/n und Diskussion.
- Es gibt nützliche Hinweise, wie man einen Vortrag hält. Bitte erstellen Sie übersichtliche Folien mit großem Schriftsatz, Grafiken und evtl. Farben.
- Betreuung: Die Vorträge sollen ausgehend von der angegebenen Literatur selbstständig erarbeitet werden. Diese soll vor allem als Startpunkt für eigene Recherche dienen, insbesondere sind die jeweiligen Bibliographien zu berücksichtigen. Das Konzept soll rechtzeitig in einem Vorgespräch diskutiert werden. Dabei können auch alle Fragen und Unklarheiten vor dem Vortrag erörtert werden.
Termine
| Datum | Thema | Vortragende/r | Literatur | Folien | Ausarbeitung | |
|---|---|---|---|---|---|---|
| 0 | 31.07.2003 | Vorbesprechung | ||||
| 1 | 14.10.2003 | Self-Testing/Correcting Programs: Einführung, Einordnung, Anwendung, Beispiele | Patrick Lauer | Designing programs that check their work und Software Reliability via Run-Time Result-Checking | Ooffice, pdf | ps |
| 2 | 21.10.2003 | Checking/Correcting Hardware | Jan Möbius | Reflections on the Pentium Division Bug und Checking the Correctness of Memories | ps | |
| 4 | 28.10.2003 | Fingerprinting techniques | Christoph Bürger | Fast probabilistic algorithms und Randomized Algorithms von Motwani/Raghavan (beides in der Bibliothek) | ||
| 5 | 11.11.2003 | Checking Probability Distributions | Le Wang | Program Checkers for Probability Generation | ||
| 7 | 18.11.2003 | Spot-checkers | Tieu Duyen Chung | Spot-checkers und Fast approximate PCPs | ||
| 8 | 25.11.2003 | IP, PCP, etc. - Einführung und Motivation wichtiger Komplexitätsklassen und ihres Zusammenhanges mit Checking | Eric Bodden | Structural Complexity I u. II (Bibliothek) und Designing programs that check their work | dvi | |
| 11 | 02.12.2003 | NP=PCP(log n,1) | Jan Henning Eckert | Wie man Beweise verifiziert, ohne sie zu lesen. | ||
| 10 | 16.12.2003 | IP=PSPACE (Weihnachtsvortrag) | Joachim Kneis | Lazlo Babai. E-mail and the unexpected power of interaction. Proceedings of the 5-th Structure in Complexity Theory, 1990 (Bibliothek) | ||
| 3 | 13.01.2004 | Kürzeste Wege (und andere Graphalgorithmen) prüfen | Fatima Zahra Laraki | LEDA Manual (bei Prof. Rossmanith, 6113) | ||
| 12 | 20.01.2004 | Checking Parallel Programs | René Nissing | Designing Checkers for Programs that run in parallel | ppt | |
| 13 | 27.01.2004 | Checking Data Structures | Daniel Schneider | Checking Linked Data Structures | ps | |
| 9 | 27.01.2003 | Checkable Languages | Jue Huang | Designing programs that check their work und The Complexity of Decision versus Search | ||
| 14 | 03.02.2004 | Self-Testing/Correcting Protocols | Carsten Rebbien | Self-Testing/Correcting Protocols. LNCS Vol. 1693/1999 (Bibliothek) | ppt | |
| 6 | 03.02.2004 | Approximate Checking | Oguzhan Oezkurt | Checking Approximate Computations over the Reals (in der Bibliothek) |