Research Group Computer Science II  Dept. of Computer Science 
Mechanized Program Verification (V4 + Ü2, SS 2003) 
Type  Times/Room  Start  Instructor 

Lecture (4)  Tue 10:00  11:30 AH III  29. 04. 2003  Prof. Dr. Jürgen Giesl 
Fri 10:00  11:30 AH II  02. 05. 2003  
Exercise (2)  Wed 11:45  13:15 AH II  07. 05. 2003  Prof. Dr. Jürgen Giesl, Darius Dlugosz 
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.
Theoretical Computer Science, Area of Specialization
