Seminar Trends in Model Checking

Seminar in Theoretical CS, Summer 2025

News

  • 16.03.2025: Added dates, more topics
  • 13.01.2025: Added Topics
  • 19.11.2024: We are online!

Introduction and Assignment of Topics

  • Coming soon.

Dates & Deadlines

Precise dates will be announced soon.

9. April 2025Kick-off meeting (room 4201b, 2nd floor, building E1)
11. April 2025Topic preferences due
5. May 2025Detailed outline and one page of content due
2. June 2025Full report due
30. June 2025Presentation slides due
7. – 10. July 2025Seminar talks (room 4201b, 2nd floor, building E1). Precise date and time to be determined

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.TopicStudentSupervisor
1van der Aalst, W.M.P., Leemans, S.J.J. (2025): Learning Generalized Stochastic Petri Nets From Event Data
2Alessandro Abate, Mirco Giacobbe, Yannik Schnitzer (2024): Bisimulation Learning
3Rajab Aghamov, Christel Baier, Toghrul Karimov, Joris Nieuwveld, Joel Ouaknine, Jakob Piribauer, Mihir Vahanwala (2025): Model Checking Markov Chains as Distribution Transformers
4Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joel Ouaknine, James Worrel (2018): Model Checking Real-Time Systems
5Kevin Batz (2024): Foundations of IC3 for Transition Systems (Section 6.1 of PhD Thesis)
6Brice, L., Bruss, F.T., Majumdar, A., Raskin, JF. (2025): Algorithms for Robbins’ Problem Using Markov Decision Processes
7Budde, C.E., D’Argenio, P.R., Fraire, J.A., Hartmanns, A., Zhang, Z. (2025): Modest Models and Tools for Real Stochastic Timed Systems
8Dimitra Giannakopoulou, Kedar S. Namjoshi, and Corina S. Pasareanu (2018): Compositional Reasoning
9Patrice Godefroid, Koushik Sen (2018): Combining Model Checking and Testing
10Jan Friso Groote, Tim A.C. Willemse (2025): On Woolhouse’s Cotton-Spinning Problem
11Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos (2025): Expectation vs. Reality: Towards Verification of Psychological Games
12Sayan 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
13Das, S., Sharma, A. (2025): Process Mining Meets Probabilistic Model Checking via Model and Logical Embeddings
14Marnix Suilen, Thom Badings, Eline M. Bovy, David Parker, Nils Jansen (2025): Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet
15Xia, Y., Cimatti, A., Griggio, A., Li, J. (2024): Avoiding the Shoals – A New Approach to Liveness Checking
16Yedi 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

Contact

mcseminar@i2.informatik.rwth-aachen.de