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

Seminar: Verifikationsverfahren

(S2, WS 2017/18)

LuFG Informatik 2


Veranstalter

Prof. Dr. Jürgen Giesl, Florian Frohn, 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 23.02.2017 ab 9:00 in Raum 4201b durchgeführt. Die genauen Zeiten sind unten angegeben. Es gelten folgende Fristen:



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", etc.).

Themen

AusarbeitungLiteraturBetreuerStudentZeit
Termination Analysis for Term Rewrite Systems Using Dependency PairsLinkProf. Dr. Jürgen GieslJiong Fu09:00-09:45
Termination Proving Through CooperationLinkDavid KorzeniewskiTom Neuhaeuser09:45-10:30
Certifying Safety and Termination Proofs for Integer Transition SystemsLinkDavid KorzeniewskiTobias Polock10:30-11:15
Proving Termination of Imperative Programs Using Max-SMTLinkMarcel HarkFabian Stein11:15-12:00
Termination Analysis by Learning Terminating ProgramsLinkJera HenselManuela Dalibor13:30-14:15
Proving Termination and Memory Safety for Programs with Pointer ArithmeticLinkJera HenselRuiming Huang14:15-15:00
Complexity Analysis for JavaLinkProf. Dr. Jürgen GieslDmytro Pachkovskyi15:00-15:45
Automated Program Verification Environment (AProVE)LinkProf. Dr. Jürgen Giesl15:45-16:00
Bounded Expectations: Resource Analysis for Probabilistic ProgramsLinkMarcel HarkFabian Niklas Meyer16:00-16:45

Vorlagen


Voraussetzungen

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



Zuordnung

Theoretische Informatik


Rückfragen

Bitte wenden Sie sich an Marcel Hark.


Disclaimer  Lehr- und Forschungsgebiet Informatik 2  Fachgruppe Informatik RWTH