Diese Seite auf Deutsch  Research Group Computer Science II  Dept. of Computer Science RWTH

Mechanized Program Verification

(V4 + Ü2, SS 2003)

LuFG Informatik II
Type Times/RoomStartInstructor
Lecture (4)Tue 10:00 - 11:30 AH III29. 04. 2003Prof. Dr. Jürgen Giesl
 Fri 10:00 - 11:30 AH II02. 05. 2003 
Exercise (2)Wed 11:45 - 13:15 AH II07. 05. 2003 Prof. Dr. Jürgen Giesl, Darius Dlugosz


In order to guarantee the reliability and correctness of programs, testing is not sufficient. Instead, a formal verification of programs is required. However, in general such verification proofs can be very costly and time-consuming. In particular, this holds for large programs used in practice.

Therefore, the goal is to mechanize program verification as much as possible. For that purpose one has to use proof tools which can verify correctness statements about programs automatically.

Thus, the course focuses on techniques to automate the task of program verification. The essential proof technique required to handle programs with loops or recursion is induction. Hence, we will introduce techniques to mechanize induction proofs for the verification of programs in a simple functional language. Moreover, we will also present methods to prove the termination of programs automatically.


The course is given in German.



Theoretical Computer Science, Area of Specialization

Last modified: Fri May 2 11:52:36 CEST 2003 / Research Group Computer Science II
RWTH Aachen