Seminar: Verifikationsverfahren

(S2, SS 2019)

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

05.04.2019: Kickoff Meeting
19.04.2019: Kontaktaufnahme mit dem Betreuer/ der Betreuerin
26.04.2019: Abmeldefrist
17.05.2019: Inhalt der Literatur verstanden haben und Konzeption absprechen
14.06.2019: Vollständige Ausarbeitung (10 Seiten inkl. Titel und Literaturverzeichnis) abgeben
Nach Absprache mit dem Betreuer aber spätestens zwei Wochen vor dem Vortrag: Vortragsfolien abgeben
Nach Absprache mit dem Betreuer aber spätestens eine Wochen vor dem Vortrag: Endgültige Version der Ausarbeitung an den Betreuer schicken.
04.09.2019 um 8:30 Uhr: Seminarvorträge in unserem Seminarraum (4201b). Der Zeitplan ist unten zu finden.

Vorgaben zur Ausarbeitung

Die Ausarbeitung kann auf Deutsch oder Englisch verfasst werden.
Die Ausarbeitung sollte folgendes Layout einhalten:
- einspaltig
- Schriftgröße 11
- Seitenränder etwa 3cm auf jeder Seite
Es sind weder ein Index noch ein Inhaltsverzeichnis erwünscht, allerdings sollte ein Literaturverzeichnis vorhanden sein.
Die Ausarbeitung darf maximal 10 Seiten inklusive Titel und Literaturangaben umfassen. Längere Ausarbeitungen werden nicht bearbeitet.
Sollte die Ausarbeitung mehr als 5 Rechtschreib- oder Grammatikfehler auf einer Seite enthalten, wird die Bearbeitung abgebrochen.
Die Ausarbeitung kann mit einem beliebigen Textverarbeitungssystem erstellt werden. Wir empfehlen allerdings LaTeX.
- Einführungsmaterial zu LaTeX aus dem LaTeX-Kurs
- Allgemeine Anmerkungen zu Ausarbeitungen und Vorträgen
Ein LaTeX-Template stellen wir nicht zur Verfügung.

Vorgaben zum Vortrag

Der Vortrag kann auf Deutsch oder Englisch gehalten werden.
Die Vortragsfolien können auf Deutsch oder Englisch verfasst werden.
Die Vortragsdauer beträgt 25 Minuten.
Die Vortragsfolien können mit einem beliebigen Präsentationprogramm erstellt 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

Title	Literature	Supervisor	Student	Time
Polynomial Orderings for Rewriting Systems	Link	Marcel Hark	Nils Freyer	08:30-09:15
Proving Termination of Term Rewriting Using Dependency Pairs	Link	Prof. Dr. Jürgen Giesl	Olav Lamberts	09:15-10:00
Termination of Integer Loops	Link	Marcel Hark	Paul Sonnenschein	10:00-10:45
Better Termination Proving Through Cooperation	Link	Stefan Dollase	Hossameldin Khalifa	10:45-11:30
Proving Termination Through Conditional Termination	Link	Marcel Hark	Yuyuan Liu	11:30-12:15
Pause				12:15-13:45
Inferring Upper Runtime Bounds for Integer Programs	Link	Prof. Dr. Jürgen Giesl	Joel Beckmann	13:45-14:30
Inferring Lower Runtime Bounds for Integer Programs	Link	Prof. Dr. Jürgen Giesl	Linus Mainka	14:30-15:15
Proving Positive Almost-Sure Termination	Link	Jera Hensel	Johannes Engelhardt	15:15-16:00
AProVE Demo	Link	Prof. Dr. Jürgen Giesl		16:00-16:15
The Symbolic Execution Debugger KeY	Link	David Korzeniewski	Thanh Nguyen	16:15-17:00

Zuordnung

Theoretische Informatik

Rückfragen

Bitte wenden Sie sich an Stefan Dollase.

Disclaimer

Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik