Theorembeweiser und ihre Anwendungen

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

Datum	Thema	Folien	Papers
21.4. (11.30h)	Einleitung	[PDF]
23.4. (8.45h)	Die Theorembeweiser dieser Welt	[PDF]	F. Wiedijk: The Seventeen Provers of the World
30.4. (8.45h)	Anwendungen in der Mathematik (1)	[PDF]	G. Gonthier: A computer-checked proof of the Four Colour Theorem
7.5. (8.45h)	Anwendungen in der Mathematik (2)	[PDF]	J. Avigad et al.: A formally verified proof of the prime number theorem W. McCune: Solution of the Robbins Problem
14.5. (8.45h)	Anwendungen in der Mathematik (3)	[PDF]	T. C. Hales: Cannonballs and honeycombs T. Nipkow et al.: Flyspeck I: Tame Graphs
28.5. (8.45h)	Protokollverifikation (1)	[PDF]	L. C. Paulson: The Inductive Approach to Verifying Cryptographic Protocols
4.6. (8.45h)	Protokollverifikation (2)	[PDF]	G. Bella, L. C. Paulson: Kerberos version IV: inductive analysis of the secrecy goals
25.6. (8.45h)	Semantik und Typsysteme (1)	[PDF]	G. Klein, T. Nipkow: A machine-checked model for a Java-like language, virtual machine, and compiler
2.7. (8.45h)	Semantik und Typsysteme (2)	[PDF]	D. Wasserrab et al.: An Operational Semantics and Type Safety Proof for Multiple Inheritance in C++
9.7. (8.45h)	Typbasierte Informationsflusskontrolle	[PDF]	D. Volpano et al.: A sound type system for secure flow analysis
16.7. (8.45h)	Compilerverifikation (1)	[PDF]	X. Leroy, S. Blazy: Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations S. Blazy et al: Formal Verification of a C Compiler Front-End
23.7. (8.45h)	Compilerverifikation (2)	[PDF]	X. Leroy: Formal certication of a compiler back-end or: programming a compiler with a proof assistant X. Leroy: A formally veried compiler back-end

Veranstalter

Lehrstuhlinhaber
Prof. Gregor Snelting

Ehemalige Mitarbeiter
Dr.-Ing. Daniel Wasserrab