|Research Group Computer Science II||Dept. of Computer Science|
Mechanized Program Verification
(V4 + Ü2, SS 2003)
|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