Teaching

Lectures

I co-organise several lectures offered by the Chair for Software Engineering.

• Cyber-Physical 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 cyber-physical, reactive systems as transition systems. We discuss different modeling formalisms, specifications in the form of linear-time properties, and the automata-theoretic approach to linear-time (LTL) model checking.

• Cyber-Physical 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 CEGAR-based 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 1-2 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 Tree-shaped Automata for Verification of Concurrent Programs BSc Thesis2023
• Computing Representative Automata for Maximal Causality Reduction MSc Thesis2022
• Statement Abstraction for POR MEd Project2022
• Owicki-Gries 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
• Owicki-Gries Correctness Proof Scheme MSc Project2021
• Clinical Guidelines Verification with ULTIMATE: A Case-Study Approach MSc Thesis2020
• Trace Abstraction with Maximal Causality Reduction MSc Thesis2020
• Large Block Encoding for Concurrent Programs BSc Thesis2019