Seminar in Theoretical CS, Winter 2023/24
News
- 17.01.2024: Seminar Talks scheduled
- 26.10.2023: Supervisors assigned
- 20.10.2023: Published student-topic assignment, fixed date for seminar talks (24.01.2024)
- 17.10.2023: Added LaTeX templates and introduction slides
- 11.09.2023: Added dates and deadlines
- 02.06.2023: We are online!
Introduction and Assignment of Topics
Dates & Deadlines
| 17.10.2023, 10:30 | Kick-off meeting (room 4201b, 2nd floor, building E1) |
| 19.10.2023 | Topic preferences due |
| 30.10.2023 | Artifact quick-check due |
| 20.11.2023 | Detailed outline and one page of content due |
| 18.12.2023 | Full report due |
| 15.01.2023 | Presentation slides due |
| 24.01.2024, 11:30 | Seminar talks (schedule below) |
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.
Seminar Talks Schedule
All seminar talks will take place on January 24 in our Seminar room (room 4201b, 2nd floor, building E1). The schedule on that day is as follows.
| 11:30-12:00 | Yujie |
| 12:00-12:30 | Niels |
| 12:30-13:00 | Thomas |
| 13:00-14:00 | Lunch break |
| 14:00-14:30 | Julius |
| 14:30-15:00 | Sinan |
| 15:00-15:30 | Femke |
Overview
Formal methods comprise techniques for the verification and analysis of digital system. Research articles in this field commonly include experimental evaluations in which implementations of newly proposed techniques are exercised on a variety of practical instances. These results are often essential for assessing performance and scalability of new approaches.
An experimental result is not fully established unless it can be independently reproduced.
Association for Computing Machinery (ACM)
The goal in this seminar is to interpret the experimental results of a selected article and to study their reproducibility using artifacts, i.e., data packages provided by the authors that include implementations, benchmarks, execution scripts, and instructions. Seminar participants get assigned one of the topics below for which they prepare a written report and a presentation that
- formally describe the considered problem statement(s) and the necessary background,
- explain relevant solution approaches using an adequate level of detail,
- outline the experiments as done by the original authors and the conclusions they made, and
- report on the reproducability of these results and the usability of the supplied artifact.
For the latter, participants run their own experiments on their machine, taking the corresponding artifact into account.
Prerequisites
Basic knowledge in Formal Languages, Automata Theory, and Mathematical Logic is expected. For some of the topics, experience with Model Checking, Formal Semantics of Programming Languages, and/or Probabilistic Programming is helpful.
Access to a standard desktop or laptop computer for running the experiments (potentially inside a virtual machine or docker container) is required. A high-end machine or computer cluster is not required–even though the original article might use one.
Some basic knowledge of Linux command line tools is often helpful but can also be attained on-the-fly.
Topics
| No. | Topic | Student | Supervisor |
|---|---|---|---|
| 1 | S. Akshay, Paul Gastin, Karthik R. Prakash: Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata. CAV 2021 (Artifact) | Femke | Tim Quatmann |
| 2 | Nicolas Amat, Silvano Dal-Zilio, Thomas Hujsa: Property Directed Reachability for Generalized Petri Nets. TACAS 2022 (Artifact) | Julius Kunstwald | Hannah Mertens |
| 3 | Nikola Benes, Lubos Brim, Samuel Pastva, David Safránek: Computing Bottom SCCs Symbolically Using Transition Guided Reduction. CAV 2021 (Artifact) | ||
| 4 | Raven Beutner, Bernd Finkbeiner: AutoHyper: Explicit-State Model Checking for HyperLTL. TACAS 2023 (Artifact) | ||
| 5 | Sebastiaan Brand, Thomas Bäck, Alfons Laarman: A Decision Diagram Operation for Reachability. FM 2023 (Artifact) | Sinan Lindemann | Tim Quatmann |
| 6 | Michele Chiari, Dino Mandrioli, Matteo Pradella Model-Checking Structured Context-Free Languages. CAV 2021 (Artifact) | ||
| 7 | Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková: Complementing Büchi Automata with Ranker. CAV 2022 (Artifact) | Yujie | Tobias Winkler |
| 8 | David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs: An O(m log n) algorithm for branching bisimilarity on labelled transition systems. TACAS 2020 (Artifact) | ||
| 9 | Peter Gjøl Jensen, Andrej Kiviriga, Kim Guldstrand Larsen, Ulrik Nyman, Adriana Mijacika, Jeppe Høiriis Mortensen: Monte Carlo Tree Search for Priced Timed Automata. QEST 2022 (Artifact) | ||
| 10 | Sebastian Junges, Matthijs T. J. Spaan: Abstraction-Refinement for Hierarchical Probabilistic Models. CAV 2022 (Artifact) | ||
| 11 | Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang: Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. CAV 2022 (Artifact) | Niels Timm | Raphaël Berthon |
| 12 | Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács: This is the moment for probabilistic loops. OOPSLA 2022 (Artifact) | ||
| 13 | Marco Paganoni, Carlo A. Furia: Verifying Functional Correctness Properties at the Level of Java Bytecode. FM 2023 (Artifact) | Thomas Schneider | Tim Quatmann |
| 14 | Long H. Pham, Jun Sun: Verifying Neural Networks Against Backdoor Attacks. CAV 2022 (Artifact) | ||
| 15 | Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett: Efficient Neural Network Analysis with Sum-of-Infeasibilities. TACAS 2022 (Artifact) |
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