Teaching
Lectures
I coorganise several lectures offered by the Chair for Software Engineering.

CyberPhysical Systems I: Discrete Models WS22/23 WS21/22 WS20/21 WS19/20
This lecture is based on the book Principles of Model Checking by Baier and Katoen, and introduces students to formal modeling of cyberphysical, reactive systems as transition systems. We discuss different modeling formalisms, specifications in the form of lineartime properties, and the automatatheoretic approach to lineartime (LTL) model checking.

CyberPhysical Systems II: Program Verification SS22 SS21 SS20 SS19
In this lecture, we develop the syntax and formal semantics of a simple imperative programming language. We use this language to introduce students to a variety of different approaches to program verification, from Hoare logic, over predicate transformers and symbolic execution, all the way to CEGARbased verification algorithms such as predicate abstraction and trace abstraction.

Theoretical Computer Science (dt: Theoretische Informatik) SS23 SS22
This course introduces students to the foundations of computation. It covers formal languages, grammars, the Chomsky hierarchy, automata theory, Turing machines, decidability and complexity theory.
Seminars
I frequently supervise students in the different seminars offered by the Chair for Software Engineering.
 Classical Articles of Program Analysis (dt: Klassische Artikel der Programmanalyse, BSc Proseminar) WS21/22 WS20/21 WS19/20
 Automata Theory (dt: Automatentheorie, BSc Proseminar / Seminar) WS22/23 SS21 SS20
 Advanced Topics in Program Analysis (MSc seminar) WS20/21
In our seminars, students are given source material on their assigned topic (either a research paper, or a book chapter). The students then write a proposal, describing their plan for a 25min research talk on the topic. Students typically review one or more proposals by other students. The talks are either given throughout the semester, or as a “block seminar” in 12 days near the end of the semester.
Student Projects
I have supervised a number of student projects revolving around program analysis and automata theory. Such projects typically involve a theoretical component (e.g. design / modification and correctness proof of some algorithm) and an implementation and evaluation component in the context of the program analysis and automata theory framework Ultimate.
If you are interested in a project or thesis, send me an email. You can find a list of possible topic areas in the Ultimate wiki.
 Computing Small Proofs for Concurrent Programs BSc Projectongoing
 Stratified Source Sets BSc Projectongoing
 Selecting Preference Orders MSc Projectongoing
 Stratified Reduction with Dynamic Abstractions BSc Thesis2023
 Dynamic Partial Order Reduction on Treeshaped Automata for Verification of Concurrent Programs BSc Thesis2023
 Computing Representative Automata for Maximal Causality Reduction MSc Thesis2022
 Statement Abstraction for POR MEd Project2022
 OwickiGries Correctness Proofs from Petri Net Unfoldings MSc Thesis2021
 Trace Abstraction Refinement with Repeated Lipton Reduction MSc Project2021
 Tight integration of Partial Order Reduction into Trace Abstraction Refinement BSc Thesis2021
 OwickiGries Correctness Proof Scheme MSc Project2021
 Clinical Guidelines Verification with ULTIMATE: A CaseStudy Approach MSc Thesis2020
 Trace Abstraction with Maximal Causality Reduction MSc Thesis2020
 Large Block Encoding for Concurrent Programs BSc Thesis2019