Konzeption
In dieser Veranstaltung wird der Einsatz von Theorembeweisern gezeigt
- sowohl theoretisch in aktuellen Forschungsthemen als auch praktisch
durch das Erlernen des Theorembeweisers
Isabelle/HOL. Zu diesem Zweck
wird die Vorlesung in eine Stunde Vorlesung und in eine Stunde
Übung unter Anleitung aufgeteilt. Die Übung dient dazu, die in der
Übung unter Anleitung vermittelten Techniken anhand von konkreten
Problemstellungen einzusetzen. Die Seite für die Übungen finden sie
hier.
Voraussetzungen
Grundkenntnisse in funktionaler Programmierung aus Info I/II,
Kenntnisse aus "Formale Systeme" sind von Vorteil.
Für die Übungen an den Rechnern im R -143 brauchen Sie einen gültigen
Studentenaccount der ATIS. Bitte prüfen Sie nach, ob ihr Account
funktioniert.
Inhalt
In der Vorlesung wird der Einsatz von Theorembeweisern in
aktuellen Forschungsthemen beleuchtet. Der Fokus liegt hierbei auf
Sprachtechnologie, es werden jedoch auch andere wichtige Themen
besprochen. In jedem Bereich werden wir aktuelle Veröffentlichungen
aus bekannten Konferenzen und Journalen betrachten.
Themen (geplant)
- Einleitung
- Die Theorembeweiser dieser Welt - eine Übersicht
- Anwendungen in der Mathematik
- Verifikation von kryptographischen Protokollen
- formale Semantiken und Typsicherheit
- Typbasierte Informationsflußkontrolle
- Verifikation eines Compiler
Bitte beachten Sie den geänderten Donnerstagstermin.
Die Vorlesung findet jetzt von 8.45 bis 9.30 statt.
Unterlagen
Termine
vom 21.04.2009,
bis 23.07.2009
| Tag |
Beginn |
Ende |
Ort |
| Donnerstag |
8:45h |
9:30h |
R -143, 50.34 |
Veranstaltungen
Veranstalter
|
