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

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:



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

TitleLiteraturBetreuerStudentUhrzeit
Termination Analysis of Integer Transition SystemsLinkDavid KorzeniewskiDamyan DimanovTBA
Termination Analysis for Term Rewrite Systems Using Dependency PairsLinkJera HenselHumam KouraniTBA
Automated Termination Proofs for Java Programs with Cyclic DataLinkStefan DollaseChristian RennertTBA
Analyzing Runtime and Size Complexity of Integer ProgramsLinkMarcel HarkPhilipp LudwigTBA
Lower Runtime Bounds for Integer ProgramsLinkProf. Dr. Jürgen GieslMarius SachsenhausenTBA
Bounded Expectations: Resource Analysis for Probabilistic ProgramsLinkMarcel HarkVincent WehrweinTBA
On Probabilistic Term RewritingLinkProf. Dr. Jürgen GieslEbru KusakTBA
Local Reasoning about Programs that Alter Data StructuresLinkStefan DollaseValentin PromiesTBA
The KeY Symbolic Execution DebuggerLinkDavid KorzeniewskiNils LommenTBA



Zuordnung

Theoretische Informatik


Rückfragen

Bitte wenden Sie sich an Marcel Hark.


Disclaimer  Lehr- und Forschungsgebiet Informatik 2  Fachgruppe Informatik RWTH