Seminar Reproducing Research Results in Formal Methods

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:30Kick-off meeting (room 4201b, 2nd floor, building E1)
19.10.2023Topic preferences due
30.10.2023Artifact quick-check due
20.11.2023Detailed outline and one page of content due
18.12.2023Full report due
15.01.2023Presentation slides due
24.01.2024, 11:30Seminar 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:00Yujie
12:00-12:30Niels
12:30-13:00Thomas
13:00-14:00Lunch break
14:00-14:30Julius
14:30-15:00Sinan
15:00-15:30Femke

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.TopicStudentSupervisor
1S. Akshay, Paul Gastin, Karthik R. Prakash: Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata. CAV 2021 (Artifact)FemkeTim Quatmann
2Nicolas Amat, Silvano Dal-Zilio, Thomas Hujsa: Property Directed Reachability for Generalized Petri Nets. TACAS 2022 (Artifact)Julius KunstwaldHannah Mertens
3Nikola Benes, Lubos Brim, Samuel Pastva, David Safránek: Computing Bottom SCCs Symbolically Using Transition Guided Reduction. CAV 2021 (Artifact)
4Raven Beutner, Bernd Finkbeiner: AutoHyper: Explicit-State Model Checking for HyperLTL. TACAS 2023 (Artifact)
5Sebastiaan Brand, Thomas Bäck, Alfons Laarman: A Decision Diagram Operation for Reachability. FM 2023 (Artifact)Sinan LindemannTim Quatmann
6Michele Chiari, Dino Mandrioli, Matteo Pradella Model-Checking Structured Context-Free Languages. CAV 2021 (Artifact)
7Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková: Complementing Büchi Automata with Ranker. CAV 2022 (Artifact)YujieTobias Winkler
8David 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)
9Peter 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)
10Sebastian Junges, Matthijs T. J. Spaan: Abstraction-Refinement for Hierarchical Probabilistic Models. CAV 2022 (Artifact)
11Yong 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 TimmRaphaël Berthon
12Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, Laura Kovács: This is the moment for probabilistic loops. OOPSLA 2022 (Artifact)
13Marco Paganoni, Carlo A. Furia: Verifying Functional Correctness Properties at the Level of Java Bytecode. FM 2023 (Artifact)Thomas SchneiderTim Quatmann
14Long H. Pham, Jun Sun: Verifying Neural Networks Against Backdoor Attacks. CAV 2022 (Artifact)
15Haoze 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

Contact

rrr23@i2.informatik.rwth-aachen.de