Summer Term 2022
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.
Theoretische Informatik (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.
Program Verification (Lecture)
Often computers are used in embedded, networked, safety critical applications. The cost of failure is high. In this lecture we introduce the basis of automatic tools for ensuring that a system does not have bad behaviours. In the lecture, we start with a short introduction to propositional logic and first-order reasoning. We then go on to establish a setting for the verification of programs, whose correctness is specified by a kind of program comments. In this setting, the correctness of the program is reduced to the validity of logical formulas. The validity is proven automatically by a new generation of powerful reasoning engines.
Softwaretechnik / Software Engineering (Lecture)
Software engineering is "the application of engineering to software" (IEEE 610.12). Goal of this course is to provide a broad overview over the challenges of software engineering and techniques and tools to overcome them. To this end, we will discuss the main activities with software development (in particular project management, requirements engineering, design, testing, formal verification) with an emphasis on formal methods. We will study process models, (software metrics), approaches to requirements specification and analysis, (formal) modeling and analysis techniques, design and architecture patterns, testing, and program verification.