Verifikationsverfahren (WS 2018/19)

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Seminar: Verifikationsverfahren
(S2, WS 2018/19)
LuFG Informatik 2

Veranstalter

Prof. Dr. Jürgen Giesl, Stefan Dollase, Marcel Hark, Jera Hensel, David Korzeniewski

Inhalt

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

Termine

Das Seminar wird als Blockseminar am 06.02.2019 ab 9:00 in Raum 4201b durchgeführt. Es gelten folgende Fristen:

26.10.2018: Kontaktaufnahme mit dem Betreuer/ der Betreuerin
31.10.2018: Abmeldefrist
16.11.2018: Inhalt der Literatur verstanden haben und Konzeption absprechen
14.12.2018: Vollständige Ausarbeitung (10 Seiten inkl. Titel und Literaturverzeichnis) abgeben
23.01.2019: Vortragsfolien abgeben
30.01.2019: Endgültige Version der Ausarbeitung an den Betreuer schicken.
06.02.2019: Seminarvorträge

Vorgaben

Die Ausarbeitung kann auf Deutsch oder Englisch verfasst werden und 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 enthalten, wird die Bearbeitung abgebrochen.

Die Vortragsdauer beträgt jeweils 25 Minuten. Die Vorträge dürfen auf Deutsch oder Englisch gehalten werden.

Voraussetzungen

Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Funktionale Programmierung", "Logikprogrammierung", "Termersetzungssysteme", "Satisfiability Checking", "Model Checking", "Statische Programmanalyse", "Semantik und Verifikation von Software", etc.).

Themen

Titel Literatur Betreuer Student Uhrzeit

Termination Analysis for Term Rewrite Systems Using Dependency Pairs Link Jera Hensel Humam Kourani 09:00-09:45

Termination Analysis of Integer Transition Systems Link David Korzeniewski Damyan Dimanov 09:45-10:30

Automated Termination Proofs for Java Programs with Cyclic Data Link Stefan Dollase Christian Rennert 10:30-11:15

Analyzing Runtime and Size Complexity of Integer Programs Link Marcel Hark Philipp Ludwig 11:15-12:00

Automated Program Verification Environment (AProVE) Link Prof. Dr. Jürgen Giesl 12:00-12:15

Bounded Expectations: Resource Analysis for Probabilistic Programs Link Marcel Hark Vincent Wehrwein 13:45-14:30

Local Reasoning about Programs that Alter Data Structures Link Stefan Dollase Valentin Promies 14:30-15:15

The KeY Symbolic Execution Debugger Link David Korzeniewski Nils Lommen 15:15-16:00

Titel	Literatur	Betreuer	Student	Uhrzeit
Termination Analysis for Term Rewrite Systems Using Dependency Pairs	Link	Jera Hensel	Humam Kourani	09:00-09:45
Termination Analysis of Integer Transition Systems	Link	David Korzeniewski	Damyan Dimanov	09:45-10:30
Automated Termination Proofs for Java Programs with Cyclic Data	Link	Stefan Dollase	Christian Rennert	10:30-11:15
Analyzing Runtime and Size Complexity of Integer Programs	Link	Marcel Hark	Philipp Ludwig	11:15-12:00
Automated Program Verification Environment (AProVE)	Link	Prof. Dr. Jürgen Giesl		12:00-12:15
Bounded Expectations: Resource Analysis for Probabilistic Programs	Link	Marcel Hark	Vincent Wehrwein	13:45-14:30
Local Reasoning about Programs that Alter Data Structures	Link	Stefan Dollase	Valentin Promies	14:30-15:15
The KeY Symbolic Execution Debugger	Link	David Korzeniewski	Nils Lommen	15:15-16:00

Zuordnung

Theoretische Informatik

Rückfragen

Bitte wenden Sie sich an Marcel Hark.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik