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

Seminar: Verifikationsverfahren

(S2, WS 2012/13)

LuFG Informatik 2


Veranstalter

Prof. Dr. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Carsten Otto, Thomas Ströder



Inhalt

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



Termine

Das Seminar wird als Blockseminar am Ende der Vorlesungszeit am 04. Februar 2013 und 05. Februar 2013 durchgeführt. Es gelten folgende Fristen:



Vorgaben

Die Ausarbeitung 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 oder mehr als zehn insgesamt enthalten, wird die Bearbeitung abgebrochen.



Voraussetzungen

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



Themen

DatumZeitOrtThemaBetreuerReferent(in)
04.02.1310:00Seminarr. i3, 4312The Dependency Pair FrameworkJ. GieslJochen Schmücking
04.02.13 10:45Seminarr. i3, 4312Proving Termination by Inductive Theorem ProvingF. EmmesThomas Heinemann
04.02.1311:30Seminarr. i3, 4312Complexity Analysis of Term Rewrite SystemsF. EmmesMoses Ganardi
04.02.1312:15Seminarr. i3, 4312Abstract Interpretation of ProgramsT. StröderNorman Hansen
04.02.1314:00Seminarr. i3, 4312Termination Analysis for Java BytecodeC. OttoEmmanuel Biver
04.02.1314:45Seminarr. i3, 4312Infeasible Code Detection for Java BytecodeC. OttoBenjamin Kaminski
05.02.1310:005052SAT Modulo TheoriesJ. GieslSebastian Roidl
05.02.1310:455052Termination Analysis by Loop SummarizationT. StröderDimitri Bohlender
05.02.1311:305052Low Level Bounded Model CheckingC. OttoKathrin Eckhardt
05.02.1312:155052Model Checking with InterpolantsM. BrockschmidtLevin Gerdes
05.02.1314:005052Automatic Generation of Loop InvariantsJ. GieslDevran Ölcer
05.02.1314:455052Verified Programming with DAFNYT. StröderPaul Smith

Die Vortragsdauer beträgt jeweils 25 Minuten.



Zuordnung

Theoretische Informatik, Informatik Vertiefung



Rückfragen

Bitte wenden Sie sich an Carsten Otto.


Disclaimer  Lehr- und Forschungsgebiet Informatik 2  Fachgruppe Informatik RWTH