The area of specialization "Programming Languages and Verification" is concerned with the theory and implementation of programming languages, and with procedures to analyze the correctness of programs in such languages. The following courses are offered.
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 introduce techniques to mechanize induction proofs for the verification of programs in a simple functional language. Moreover, we also present methods to prove the termination of programs automatically.
The course gives an introduction to functional programming using the language Haskell. Moreover, we discuss models for the semantics and the implementation of functional languages. This also includes techniques for type checking and type inference as well as methods for the optimization of functional programs.
Term rewriting systems are used for computations and mechanized proofs with equations. All functional programming languages are based on term rewriting systems, too. Therefore, term rewriting systems are used in many areas like mechanized program verification, specification of programs and declarative programming. The following questions will be discussed in the course.
Apart from a short introduction to the programming language Prolog this course is concerned with the basics of logic programming, programming techniques and implementations of logic programming languages.