This page in English  Lehr- und Forschungsgebiet Informatik 2  Fachgruppe Informatik RWTH

Seminar: Verifikationsverfahren

(S2, SS 2019)

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 Ende des Semesters durchgeführt. Es gelten folgende Fristen:



Vorgaben zur Ausarbeitung



Vorgaben zum Vortrag



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

TitleLiteratureSupervisorStudentTime
The Symbolic Execution Debugger KeY Link David Korzeniewski Thanh Nguyen TBA
Proving Termination Through Conditional Termination Link Marcel Hark Yuyuan Liu TBA
Polynomial Orderings for Rewriting Systems Link Marcel Hark Nils Freyer TBA
Termination of Integer Loops Link Marcel Hark Paul Sonnenschein TBA
Termination Analysis of Imperative Programs using Bitvector Arithmetic Link Jera Hensel Martin Hashem TBA
Proving Positive Almost-Sure Termination Link Jera Hensel Johannes Engelhardt TBA
Proving Termination of Term Rewriting Using Dependency Pairs Link Prof. Dr. Jürgen Giesl Olav Lamberts TBA
Inferring Upper Runtime Bounds for Integer Programs Link Prof. Dr. Jürgen Giesl Joel Beckmann TBA
Inferring Lower Runtime Bounds for Integer Programs Link Prof. Dr. Jürgen Giesl Linus Mainka TBA
Better Termination Proving Through Cooperation Link Stefan Dollase Hossameldin Khalifa TBA



Zuordnung

Theoretische Informatik


Rückfragen

Bitte wenden Sie sich an Stefan Dollase.


Disclaimer  Lehr- und Forschungsgebiet Informatik 2  Fachgruppe Informatik RWTH