Seminar Trends in Model Checking

Seminar in Theoretical CS, Summer 2024

News

  • 07.06.2024: The seminar talks will take place on 24.07.2024 at 09:00 in the i2 Seminar room 4201b
  • 15.04.2024: Student topic and supervisor assignment added.
  • 12.04.2024: Slides of introduction and LaTeX templates added.
  • 09.04.2024: Topics added.
  • 05.12.2023: We are online!

Introduction and Assignment of Topics

Dates & Deadlines

12.04.2024, 10:30Kick-off meeting (room 4201b, 2nd floor, building E1)
15.04.2024Topic preferences due
06.05.2024Detailed outline and one page of content due
10.06.2024Full report due
15.07.2024Presentation slides due
24.07.2024, 09:00Seminar talks (room 4201b, 2nd floor, building E1)

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

The topic assignment will be explained in the Kickoff Meeting on April 12

No.TopicStudentSupervisor
1Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y., Wells, A. (2023). Model Checking Strategies from Synthesis over Finite Traces.
2Finkbeiner, B., Rabe, M.N., Sánchez, C. (2015). Algorithms for Model Checking HyperLTL and HyperCTL.
3Hartmanns, A. (2022). Correct Probabilistic Model Checking with Floating-Point Arithmetic.
4Jakobsen, A.B., Jørgensen, R.S.M., van de Pol, J., Pavlogiannis, A. (2024). Fast Symbolic Computation of Bottom SCCs.Jan Erik KarucAlexander Bork
5König, L. et al. (2024). Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development.Hiya MandalAlexander Bork
6Martens, J. et al. (2023) Linear parallel algorithms to compute strong and branching bisimilarity.
7Osama, M., Wijs, A. (2024). Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking.
8Sickert, S., Esparza, J., Jaax, S., Křetínský, J. (2016). Limit-Deterministic Büchi Automata for Linear Temporal Logic.Tobias ArensTim Quatmann
9Volk, M., Junges, S., Katoen, J.-P. (2017). Fast Dynamic Fault Tree Analysis by Model Checking Techniques.

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

mcseminar24@i2.informatik.rwth-aachen.de