Verifikationsverfahren (WS 2010/2011)

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Verifikationsverfahren
(S2, WS 2010/2011)
LuFG Informatik 2

Veranstalter

Prof. Dr. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Carsten Fuhs, Carsten Otto, Thomas Ströder

Inhalt

In diesem Seminar werden verschiedene Techniken und Verfahren zur Verifikation von Programmen vorgestellt.

Termine

Das Seminar wird als Blockseminar am Ende der Vorlesungszeit im Februar 2011 durchgeführt. Es gelten folgende Fristen:

02.11.2010: Literatur abholen
29.11.2010: Inhalt der Literatur verstanden haben und Konzeption absprechen
20.12.2010: Vollständige Ausarbeitung (10 Seiten inkl. Titel und Literaturverzeichnis) abgeben
15.02.2011: Tag des Seminars. Hierzu sollen Sie die korrigierte Ausarbeitung in ausreichender Anzahl kopiert mitbringen; die Kopien können am Lehr- und Forschungsgebiet angefertigt werden

Vorgaben

Die Ausarbeitung darf nicht mehr als 10 Seiten inklusive Titel und Literaturverzeichnis umfassen. Bei diesem Umfang sind weder ein Index noch ein Inhaltsverzeichnis erwünscht, allerdings sollte ein Literaturverzeichnis vorhanden sein. Sollte die Ausarbeitung mehr als fünf Rechtschreib- oder Grammatikfehler auf einer Seite oder mehr als zehn insgesamt enthalten, wird die Bearbeitung abgebrochen.

Voraussetzungen

Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Logikprogrammierung", "Funktionale Programmierung", "Termersetzungssysteme", "Automatisierte Programmverifikation").

Themen

Datum Zeit Thema Betreuer Referent(in)

15.02. 10:00 SAT + SMT Solving C. Fuhs Thomas Freese

15.02. 10:45 Low Level Bounded Model Checking T. Ströder Michael Kurze

15.02. 13:00 Java Bytecode Verification C. Otto Peng Sun

15.02. 13:45 Verification of Imperative Programs with KeY M. Brockschmidt Lucas Brutschy

15.02. 14:30 Programming with Dependent Types F. Emmes Max Goertz

Datum	Zeit	Thema	Betreuer	Referent(in)
15.02.	10:00	SAT + SMT Solving	C. Fuhs	Thomas Freese
15.02.	10:45	Low Level Bounded Model Checking	T. Ströder	Michael Kurze
15.02.	13:00	Java Bytecode Verification	C. Otto	Peng Sun
15.02.	13:45	Verification of Imperative Programs with KeY	M. Brockschmidt	Lucas Brutschy
15.02.	14:30	Programming with Dependent Types	F. Emmes	Max Goertz

Die Vortragsdauer beträgt jeweils 30 Minuten. Alle Startzeiten sind vorläufig.

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Rückfragen

Bitte wenden Sie sich an Thomas Ströder.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik