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

Contents

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.

Language

References

• C. Walther: Mathematical Induction. In "Handbook of Logic in Artificial Intelligence and Logic Programming", Vol. 2, D.M. Gabbay, C.J. Hogger, J.A. Robinson (eds.), Oxford University Press, pages 127-227, 1994.
• T. Arts and J. Giesl: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science, 236:133-178, 2000.
• A. Bundy: The Automation of Proof by Mathematical Induction. In "Handbook of Automated Reasoning", J.A. Robinson, A. Voronkov (ed.), Elsevier & MIT Press, pages 845-911, 2001.
• K.H. Bläsius & H.-J. Bürckert: Deduktionssysteme. Oldenbourg Verlag, 1992.

Area

Theoretical Computer Science, Area of Specialization

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