Winter Term 2015/16
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.
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.
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.
Software Design, Modelling, and Analysis in UML (Lecture)
The model-driven approach to software and systems development proposes to address quality and complexity issues in the development process. The usage of modelling languages not only for documentation, but, e.g., for automated analysis, test generation, and code generation is gaining momentum in particular in the context of (safety) critical software development. The necessary pre-requisites are a semantically founded modelling language and methods and tools for analysis. We will take the Unified Modelling Language (UML) as an example and demonstrate how to equip a relevant sublanguage (sometimes referred to as executable core) with a precise meaning in line with the official standard documents. To complement these discussions, we provide access to a contemporary UML modelling tool and use it for some of the exercises.