Seminar in Theoretical CS, Summer 2025
News
- 18.04.2025: Date for Seminar Talks Fixed
- 14.04.2025: Supervisors Assigned
- 11.04.2025: Topics Assigned, Kickoff Meeting Slides uploaded
- 16.03.2025: Added dates, more topics
- 13.01.2025: Added Topics
- 19.11.2024: We are online!
Introduction and Assignment of Topics
- See Slides from Kickoff Meeting
Dates & Deadlines
Precise dates will be announced soon.
| 9. April 2025 | Kick-off meeting (room 4201b, 2nd floor, building E1) |
| 11. April 2025 | Topic preferences due |
| 5. May 2025 | Detailed outline and one page of content due |
| 2. June 2025 | Full report due |
| 30. June 2025 | Presentation slides due |
| 9. July 2025 | 9:00 – 15:00. Seminar talks (room 4201b, 2nd floor, building E1). Schedule will be announced a few days before the seminar |
Note that the full versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.
Overview
Model checking is an automatic verification technique for both software and hardware systems. It systematically checks a given model representing the system under consideration (such as a finite labelled transition system) satisfies a property (e.g., a safety requirement) and thus verifies if that system has the expected behaviour. If this is not the case, diagnostic information is given in the form of counterexamples.
This seminar aims to give an overview of the research in the field of model checking. Each topic is covered by a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation. The presentations will be given at the end of the lecture period as a block seminar.
Prerequisites
Basic knowledge in Formal Languages, Automata Theory, and Mathematical Logic is expected. Experience with Model Checking and/or verification of probabilistic systems is helpful.
Topics
All topics are based on one of the scientific papers below.
Note that some of the papers are part of the Festschrift dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday.
| No. | Topic | Student | Supervisor |
|---|---|---|---|
| 1 | van der Aalst, W.M.P., Leemans, S.J.J. (2025): Learning Generalized Stochastic Petri Nets From Event Data | Ha Dang | Emma Ahrens |
| 2 | Alessandro Abate, Mirco Giacobbe, Yannik Schnitzer (2024): Bisimulation Learning | Felipe Bönnen | Emma Ahrens |
| 3 | Rajab Aghamov, Christel Baier, Toghrul Karimov, Joris Nieuwveld, Joel Ouaknine, Jakob Piribauer, Mihir Vahanwala (2025): Model Checking Markov Chains as Distribution Transformers | Frederic Busch | Raphaël Berthon |
| 4 | Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joel Ouaknine, James Worrel (2018): Model Checking Real-Time Systems | Johannes Kurth | Raphaël Berthon |
| 5 | Kevin Batz (2024): Foundations of IC3 for Transition Systems (Section 6.1 of PhD Thesis) | Stanislas Briaud | Darion Haase |
| 6 | Brice, L., Bruss, F.T., Majumdar, A., Raskin, JF. (2025): Algorithms for Robbins’ Problem Using Markov Decision Processes | ||
| 7 | Budde, C.E., D’Argenio, P.R., Fraire, J.A., Hartmanns, A., Zhang, Z. (2025): Modest Models and Tools for Real Stochastic Timed Systems | ||
| 8 | Dimitra Giannakopoulou, Kedar S. Namjoshi, and Corina S. Pasareanu (2018): Compositional Reasoning | ||
| 9 | Patrice Godefroid, Koushik Sen (2018): Combining Model Checking and Testing | Pavlo Viberg | Darion Haase |
| 10 | Jan Friso Groote, Tim A.C. Willemse (2025): On Woolhouse’s Cotton-Spinning Problem | ||
| 11 | Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos (2025): Expectation vs. Reality: Towards Verification of Psychological Games | ||
| 12 | Sayan Mitra, Corina PƒÉsƒÉreanu, Pavithra Prabhakar, Sanjit A. Seshia, Ravi Mangal, Yangge Li, Christopher Watson, Divya Gopinath & Huafeng Yu (2025): Formal Verification Techniques for Vision-Based Autonomous Systems | Sönke Köster | Raphaël Berthon |
| 13 | Das, S., Sharma, A. (2025): Process Mining Meets Probabilistic Model Checking via Model and Logical Embeddings | Gustavo Lopez Ramirez | Emma Ahrens |
| 14 | Marnix Suilen, Thom Badings, Eline M. Bovy, David Parker, Nils Jansen (2025): Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet | Peter Lindner | Darion Haase |
| 15 | Xia, Y., Cimatti, A., Griggio, A., Li, J. (2024): Avoiding the Shoals – A New Approach to Liveness Checking | ||
| 16 | Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Taolue Chen (2021): BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks |
Registration
Registration to the seminar is handled via the SuPra system.
Grading Scheme
You can access the grading scheme here: https://moves.rwth-aachen.de/wp-content/uploads/seminar_grading_scheme.pdf
Additional Material
- LaTeX templates for report and presentation
- How to Write a Seminar Paper
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- How to Give Presentations
- Introduction to LaTeX