181.221 Seminar Formale Methoden
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2020W, SE, 2.0h, 3.0EC
Quinn ECTS Erhebung


  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: SE Seminar
  • Format der Abhaltung: Online


Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

- read scientific papers,
- understand the content as well as the significance of a paper,
- literature research,
- present scientific work in an accessible manner

Inhalt der Lehrveranstaltung

The seminar covers selected topics in the field of formal methods. The course revolves around seminal research papers in the field of automated reasoning and computer-aided verification.  Each student will be assigned one research paper. The students are expected to read and understand the paper and prepare and present a half-hour talk on the topic. 



Proposed list of papers: 

Papers proposed and to be supervised by Georg Weissenbacher: 

  • Gagandeep Singh, Timon Gehr, Markus Püschel, Martin T. Vechev: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL): 41:1-41:30 (2019) https://doi.org/10.1145/3290354 
  • Erika Ábrahám, Borzoo Bonakdarpour: HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties. QEST 2018: 20-35 https://arxiv.org/abs/1804.01853
  • William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac: Lazy counterfactual symbolic execution. PLDI 2019: 411-424 https://doi.org/10.1145/3314221.3314618 
  • Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, Klaus Wehrle: Symbolic Partial-Order Execution for Testing Multi-Threaded Programs. CAV (1) 2020: 376-400 https://doi.org/10.1007/978-3-030-53288-8_18

Papers proposed and to be supervised by Florian Zuleger

  • Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham: Reducing liveness to safety in first-order logic. PACMPL 2(POPL) 2018: 26:1-26:33 
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier: The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS 2019: 242-259
  • Jérôme Leroux, Sylvain Schmitz: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. LICS 2019: 1-13 
  • Christian Müller, Helmut Seidl, Eugen Zalinescu: Inductive Invariants for Noninterference in Multi-agent Workflows. CSF 2018: 247-261



The first objective is to read and understand the content as well as the significance of the assigned paper, and read up on related work if the paper is not self-contained. Prior to preparing the presentation, students are expected to discuss the papers in a meeting with the lecturer.

The objectives of the presentation are to present the topic in a manner accessible for their fellow students. Students are required to present and discuss their slides with the lecturer prior to giving the presentation.



Weitere Informationen


How to give a good talk (by Simon Peyton Jones, given in Vienna, October 2004):


(requires Real Player)

Beachten Sie beim Verfassen der Ausarbeitung bitte die Richtlinie der TU Wien zum Umgang mit Plagiaten: Leitfaden zum Umgang mit Plagiaten (PDF)

Vortragende Personen


LVA Termine

Mi.10:00 - 10:4521.10.2020 Seminar room Menger, Favoritenstrasse 9-11, 3rd floorFM Seminar - Introduction, Organization
Mo.09:00 - 12:3014.12.2020 Seminar room Menger, Favoritenstrasse 9-11, 3rd floorStudent presentations


Students will be graded based on:

1.) Ability to read and understand the papers assigned to them. The
effort and initiative to independently read and understand the paper 
and to read up on related work will determine 50% of the grade. The
students' understanding of the paper will be evaluated during the
meetings with the lecturer and by means of questions after the talk.

2.) Ability to present the material in an accessible way to their fellow
students. The clarity and style of the presentation as well as the
students' effort to prepare the talk (e.g., by designing their own
examples rather than reusing material from the paper) determine 50% of 
the grade.

Additional information on grading: The relative difficulty of the
paper will be taken into account. Asking meaningful questions about
the presentations of fellow students will have a positive impact
on the grade (attendance of these talks is compulsory).


ECTS Breakdown:
40 hours for reading papers and related work, 
20 hours for preparing the presentation, 
15 hours of attending talks and meetings with the lecturer.
75 hours (3 ECTS)



  • October 13, 13:00-14:00: Initial meeting, online
  • October 13 - Nov 30: Individual meetings between students and seminar responsibles, online
  • Dec 1: Student presentations (if this date does not work for all seminar participants, we will choose a date a few days earlier or later)


The topics and the organization of the seminar will be discussed during an initial meeting on October 13, 13:00-14:00, online. (If you can not attend this initial meeting you should contact florian.zuleger@tuwien.ac.at as soon as possible).

Students can choose a paper by sending an email to florian.zuleger@tuwien.ac.at.

Students are expected to read the chosen papers, search relevant literature (reading related papers) and prepare a scientific presentation on the paper.

Students are expected two have at least two individual meetings with their supervisor, discussing the content of the paper, the outline of the presentation and the details of the presentation.

Student presentations will take place during Dec 1 (if this date does not work for all seminar participants, we will choose a date a few days earlier or later).


Von Bis Abmeldung bis
02.09.2020 00:00 13.10.2020 23:59 20.10.2020 23:59


066 504 Masterstudium Embedded Systems Keine Angabe
066 931 Logic and Computation Gebundenes Wahlfach
066 937 Software Engineering & Internet Computing Gebundenes Wahlfach


Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Weitere Informationen

  • Anwesenheitspflicht!