Verifikationsverfahren (WS 2012/13)

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Verifikationsverfahren
(S2, WS 2012/13)
LuFG Informatik 2

Veranstalter

Prof. Dr. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, 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 am 04. Februar 2013 und 05. Februar 2013 durchgeführt. Es gelten folgende Fristen:

29.10.2012: Literatur abholen
26.11.2012: Inhalt der Literatur verstanden haben und Konzeption absprechen
17.12.2012: Vollständige Ausarbeitung (10 Seiten inkl. Titel und Literaturverzeichnis) abgeben
04/05.02.13: 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. "Funktionale Programmierung", "Termersetzungssysteme", "Logikprogrammierung").

Themen

Datum Zeit Ort Thema Betreuer Referent(in)

04.02.13 10:00 Seminarr. i3, 4312 The Dependency Pair Framework J. Giesl Jochen Schmücking

04.02.13 10:45 Seminarr. i3, 4312 Proving Termination by Inductive Theorem Proving F. Emmes Thomas Heinemann

04.02.13 11:30 Seminarr. i3, 4312 Complexity Analysis of Term Rewrite Systems F. Emmes Moses Ganardi

04.02.13 12:15 Seminarr. i3, 4312 Abstract Interpretation of Programs T. Ströder Norman Hansen

04.02.13 14:00 Seminarr. i3, 4312 Termination Analysis for Java Bytecode C. Otto Emmanuel Biver

04.02.13 14:45 Seminarr. i3, 4312 Infeasible Code Detection for Java Bytecode C. Otto Benjamin Kaminski

05.02.13 10:00 5052 SAT Modulo Theories J. Giesl Sebastian Roidl

05.02.13 10:45 5052 Termination Analysis by Loop Summarization T. Ströder Dimitri Bohlender

05.02.13 11:30 5052 Low Level Bounded Model Checking C. Otto Kathrin Eckhardt

05.02.13 12:15 5052 Model Checking with Interpolants M. Brockschmidt Levin Gerdes

05.02.13 14:00 5052 Automatic Generation of Loop Invariants J. Giesl Devran Ölcer

05.02.13 14:45 5052 Verified Programming with DAFNY T. Ströder Paul Smith

Datum	Zeit	Ort	Thema	Betreuer	Referent(in)
04.02.13	10:00	Seminarr. i3, 4312	The Dependency Pair Framework	J. Giesl	Jochen Schmücking
04.02.13	10:45	Seminarr. i3, 4312	Proving Termination by Inductive Theorem Proving	F. Emmes	Thomas Heinemann
04.02.13	11:30	Seminarr. i3, 4312	Complexity Analysis of Term Rewrite Systems	F. Emmes	Moses Ganardi
04.02.13	12:15	Seminarr. i3, 4312	Abstract Interpretation of Programs	T. Ströder	Norman Hansen
04.02.13	14:00	Seminarr. i3, 4312	Termination Analysis for Java Bytecode	C. Otto	Emmanuel Biver
04.02.13	14:45	Seminarr. i3, 4312	Infeasible Code Detection for Java Bytecode	C. Otto	Benjamin Kaminski
05.02.13	10:00	5052	SAT Modulo Theories	J. Giesl	Sebastian Roidl
05.02.13	10:45	5052	Termination Analysis by Loop Summarization	T. Ströder	Dimitri Bohlender
05.02.13	11:30	5052	Low Level Bounded Model Checking	C. Otto	Kathrin Eckhardt
05.02.13	12:15	5052	Model Checking with Interpolants	M. Brockschmidt	Levin Gerdes
05.02.13	14:00	5052	Automatic Generation of Loop Invariants	J. Giesl	Devran Ölcer
05.02.13	14:45	5052	Verified Programming with DAFNY	T. Ströder	Paul Smith

Die Vortragsdauer beträgt jeweils 25 Minuten.

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Rückfragen

Bitte wenden Sie sich an Carsten Otto.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik