Verification Techniques (WS 2002/2003)

Seminar: Verification Techniques
(S2, WS 2002/2003)
LuFG Informatik II

Instructor

Prof. Dr. Jürgen Giesl, Darius Dlugosz, René Thiemann

Times

The seminar will take place on two days at the end of the semester (February 2003). The first preliminary meeting is on Friday, October 25, 2002, in the lecture hall AH I at 11:45-13:15.

Registration

Students interested in the seminar should contact Prof. Dr. Jürgen Giesl ( giesl@informatik.rwth-aachen.de, Tel: 80-21230).

Prerequisites

Participants should have some knowledge in program verification or related areas (for example "term rewriting", "mechanized program verification", or "functional programming"). It is also possible to attend the course on "functional programming" this semester.

References

The books and papers to be discussed in the seminar will be announced at the preliminary meeting.

Several techniques and methods for program verification will be presented in this seminar. More precisely, we will deal with the following topics:

Zeit Datum Thema Referent(in)

9:30 Mo., 17.2. Terminierungsanalyse von Termersetzungssystemen mit Dependency Pairs Stephan Palm
10:45 Mo., 17.2. Terminierungsanalyse von Higher-Order Termersetzungssystemen Diego Biurrun
12:00 Mo., 17.2. Terminierungsanalyse von funktionalen Programmen mit Lazy Evaluation Frank Peiffer
14:00 Mo., 17.2. Terminierungsanalyse von funktionalen Programmen durch Size-Change Graphen Michael Sauren
15:15 Mo., 17.2. Terminierungsanalyse von logischen Programmen Niklas Mausberg
9:30 Di., 18.2. Explizite Induktionsbeweisverfahren Barbara Friemann
10:45 Di., 18.2. Implizite Induktionsbeweisverfahren Salaheddine Benyassine
12:00 Di., 18.2. Induktionsverfahren zur Protokollverifikation Christof Skrzypczyk
14:00 Di., 18.2. Protokollverifikation mit Termersetzungstechniken Thomas Schoenemann
15:15 Di., 18.2. Verifikation von logischen Programmen Nils Wilhelms
16:30 Di., 18.2. Proof-Carrying Code Ingo Zander

Zeit	Datum	Thema	Referent(in)
9:30	Mo., 17.2.	Terminierungsanalyse von Termersetzungssystemen mit Dependency Pairs	Stephan Palm
10:45	Mo., 17.2.	Terminierungsanalyse von Higher-Order Termersetzungssystemen	Diego Biurrun
12:00	Mo., 17.2.	Terminierungsanalyse von funktionalen Programmen mit Lazy Evaluation	Frank Peiffer
14:00	Mo., 17.2.	Terminierungsanalyse von funktionalen Programmen durch Size-Change Graphen	Michael Sauren
15:15	Mo., 17.2.	Terminierungsanalyse von logischen Programmen	Niklas Mausberg
9:30	Di., 18.2.	Explizite Induktionsbeweisverfahren	Barbara Friemann
10:45	Di., 18.2.	Implizite Induktionsbeweisverfahren	Salaheddine Benyassine
12:00	Di., 18.2.	Induktionsverfahren zur Protokollverifikation	Christof Skrzypczyk
14:00	Di., 18.2.	Protokollverifikation mit Termersetzungstechniken	Thomas Schoenemann
15:15	Di., 18.2.	Verifikation von logischen Programmen	Nils Wilhelms
16:30	Di., 18.2.	Proof-Carrying Code	Ingo Zander

Area

Theoretical Computer Science, Area of Specialization