Seminar Trends in Model Checking

Seminar in Theoretical CS, Summer 2026

News

  • 14.01.2025: Seminar Topics
  • 11.12.2025: We are online!

Introduction and Assignment of Topics

Available after Kickoff Meeting

Seminar Talks Schedule

All Presentations will be given on one or two days in July (precise date to be announced) in the i2 Seminar Room (room 4201b, 2nd floor, building E1)

Dates & Deadlines

Precise dates will be announced soon.

approx 17. April 2026Kick-off meeting (room 4201b, 2nd floor, building E1)
20. April 2026Topic preferences due
11. May 2025Detailed outline and one page of content due
8. June 2025Full report due
6. July 2025Presentation slides due
?. July 202610:30 – 14:30. Seminar talks (room 4201b, 2nd floor, building E1). Schedule above

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.
(MORE TOPICS ARE ADDED ON DEMAND)

Model Checking Algorithms

  1. Finkbeiner, B., Rabe, M.N., Sánchez, C. (2015): Algorithms for Model Checking HyperLTL and HyperCTL.
  2. Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y., Wells, A. (2023): Model Checking Strategies from Synthesis over Finite Traces.

State Space Reduction Techniques

  1. Herbreteau, F., Larroze-Jardiné, S., Point, G., Walukiewicz, I. (2024): Revisiting Stateful Partial-Order Reduction.
  2. Abate, A., Giacobbe, M., Schnitzer, Y. (2024): Bisimulation learning.

Symbolic Model Checking

  1. Zhang, Y., Zhao, Z., Chen, G., Song, F., Chen, T. (2021): BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks.
  2. Xia, Y., Cimatti, A., Griggio, A., Li, J. (2024): Avoiding the Shoals – A New Approach to Liveness Checking.
  3. Souri, A., Rahmani, A.M., Jafari Navimipour, N., Rezaei, R. (2019): A symbolic model checking approach in formal verification of distributed systems.

Probabilistic Model Checking

  1. Hartmanns, A. (2022): Correct Probabilistic Model Checking with Floating-Point Arithmetic.
  2. Meggendorfer, T., Weininger, M., Wienhöft P. (2025): Solving Robust Markov Decision Processes: Generic, Reliable, Efficient.
  3. Spork,T.; Baier,C.; Katoen,J.-P.; Klüppelholz,S.; Piribauer,J. (2025): Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains.

Registration

Registration to the seminar is handled via the SuPra system.

Additional Material

Contact

mcseminar@i2.informatik.rwth-aachen.de