Winter Term 2017/18
Automata Theory (Seminar, Proseminar)
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.
Program Analysis & Software Testing (Seminar)
Program analysis is the research area that studies the automatic analysis of computer programs. The methods that are developed in this research area e.g., help programmers to understand complex programs, allow compilers to optimize their code, and enable computers to check the correctness of programs. In this seminar each student will study a research paper and give a talk in which he/she presents a summary of the paper.
Softwarepraktikum (Nicht für B.Sc. Informatik und B. Sc. ESE)
In diesem Praktikum soll ein Softwareentwicklungsprozess, beginnend bei Anforderungserhebung über Entwurfsphase bis hin zur Implementierung, die Organisation der Arbeit innerhalb einer Gruppe und der Umgang mit komplexen Systemen erlernt werden. Die Teilnehmer werden von den Betreuern in Gruppen eingeteilt und müssen eine bestimmte Aufgabenstellung realisieren. Hierzu müssen sie sich selbst organisieren, die Anforderungen definieren, Arbeit geschickt auf Gruppenmitglieder verteilen und neue Technologien selbstständig erlernen.
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.
Informatik III (Lecture)
Die Vorlesung gibt eine Einführung in die Theoretische Informatik. Sie führt in die Themen Endliche Automaten, Formale Sprachen und Grammatiken ein und liefert mehrere äquivalente präzise Fassungen des Berechenbarkeitsbegriffs. Es schließt sich eine Einführung in die Komplexitätstheorie, speziell die Theorie der NP-Vollständigkeit, an. Behandelt werden abstrakte Modelle von Maschinen und Sprachen und mit ihrer Hilfe werden Komplexitätsmaße wie Schrittzahl (Laufzeit) und Speicherbedarf von Algorithmen präzise definiert.
Real-Time Systems (Lecture)
Real-time systems need to react to certain input stimuli within given time bounds. For example, an airbag in a car has to unfold within 300 milliseconds in a crash. There are many embedded safety-critical applications and each requires real-time specification techniques. We will study and apply some of these techniques, based on logic and automata, most prominently timed automata.