I co-organise several lectures offered by the Chair for Software Engineering.
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.
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.
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.
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.
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