Winter Term 2019/20
Automata Theory (Seminar)
In the lecture about theoretical computer science you have seen finite automata, pushdown automata and Turing machines. All three of them operate on finite words. However there are other automata models and automata that do not operate on finite words, but e.g. on infinite words, on nested words, on trees, etc. In this seminar we will have a look at automata models that you have not seen in the lecture on theoretical computer science.
Decision Procedures (Lecture)
Decision Procedures are the basis for program verification: The task of program verification is to give a formal proof that a program meets its specification. This amounts to determining the truth value of a logical formula. A decision procedure is an algorithm that can for a certain type of formulas decide whether the formula is true or false. We will investigate decision procedures for different logics. Starting with propositional logic we will investigate decision procedures for logics with integers, reals, recursive structures (lists and trees), arrays, etc.
Cyber-Physical Systems I - Discrete Models (Lecture)
Model checking is a technique for the automatic verification of hardware or software systems. Given such a system and a specification of its intended behaviour, a model checker finds out whether the system satisfies the specification. Model checking has made enormous progress since its invention in the 1980s; today it is possible to verify entire CPU designs, and so all major microprocessor companies use and develop tools for this purpose. Software verification is more challenging than hardware verification and an active research topic (pursued at the chair for Software Engineering, for instance!). Recent years have seen interesting progress in this area as well. The industry has already started using these techniques to check, e.g., safety-critical embedded systems, and software libraries; yet, many research challenges, both theoretical and practical, lie ahead of us.
Programmanalyse (Proseminar)
In this proseminar, we will study a selection of articles which can be considered classical (or fundamental) for the topic area program analysis. The articles have been published between 1938 and 2009 and some of the authors received the acknowledged Turing Award for their work. We will have weekly sessions starting early November (so not an "en bloc" schedule). The available topics will be introduced in the first session, together with the modus operandi (schedule, deliverables, grades).