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

The seminar covers selected topics in the field of formal methods. The course revolves around seminal research papers in the fields of program analysis, 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. 

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.

RESOURCES:

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

http://research.microsoft.com/en-us/um/people/simonpj/papers/giving-a-talk/giving-a-talk.htm

(requires Real Player)

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)
---------------------------------------

PAPER ASSIGNMENT:

1) Marton Hajdu: Simon Cruanes: Superposition with Structural Induction. FroCoS 2017: 172-188

Supervision: Laura Kovacs

2) Timothee Durand: Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup: Verifying Hyperliveness, CAV 2019 (https://doi.org/10.1007/978-3-030-25540-4_7)

Supervision: Georg Weissenbacher

3) Samuel Pilz: Programming and Proving with Distributed Protocols

Supervision: Pavol Cerny

4) Stefan Zaruba: Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey: A true positives theorem for a static race detector. PACMPL 3(POPL) 2019: 57:1-57:29

Supervision: Florian Zuleger

5) Emre Kurtulus: Verifying Array Manipulating Programs with Full-Program Induction. CoRR abs/2002.09857 (2020).

Supervision: Laura Kovacs

6) Mathias Hofer: Bas Ketsman, Aws Albarghouthi and Paraschos Koutris: Distribution Policies for Datalog. ICDT 18 Database Theory: 17:1-17:22

Supervision: Pavol Cerny

PAPERS to choose from:

Papers proposed and to be supervised by Laura Kovacs: 

• Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat: Verifying Array Manipulating Programs with Full-Program Induction. CoRR abs/2002.09857 (2020). Accepted at TACAS 2020.
• Simon Cruanes: Superposition with Structural Induction. FroCoS 2017: 172-188
• Azadeh Farzan, Anthony Vandikas: Automated Hypersafety Verification. CAV (1) 2019: 200-218

Papers proposed and to be supervised by Pavol Černý: 

• SNAP: Stateful network-wide abstractions for packet processing M Arashloo, Y Koral, M Greenberg, J Rexford, D Walker
  SIGCOMM 2016 
• Ilya Sergey, James R. Wilcox, and Zachary Tatlock, Programming and Proving with Distributed Protocols (POPL ‘18)
• K. Mamouras, M. Raghothaman, R. Alur, Z. Ives, and S. Khanna. StreamQRE: Modular specification and efficient evaluation of quantitative queries over streaming data, ACM Conference on Programming Language Design and Implementation, 2017. 

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 
• Christian Müller, Helmut Seidl, Eugen Zalinescu: Inductive Invariants for Noninterference in Multi-agent Workflows. CSF 2018: 247-261
• Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey: A true positives theorem for a static race detector. PACMPL 3(POPL) 2019: 57:1-57:29 

Papers proposed and to be supervised by Georg Weissenbacher

• Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup: Verifying Hyperliveness, CAV 2019 (https://doi.org/10.1007/978-3-030-25540-4_7)
• Bernd Finkbeiner, Martin Zimmermann: The First-Order Logic of Hyperproperties. STACS 2017 (https://doi.org/10.4230/LIPIcs.STACS.2017.30)
• Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi: Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. IJCAI 2016 (http://www.ijcai.org/Abstract/16/503)

ORGANISATION:

The topics and the organization of the seminar will be discussed during the initial meeting on 16.3., 13:00, in the Menger meeting room (Favoritenstrasse 9, 3rd floor).

Students signed up for the course who are unable to attend should contact us as soon as possible.

Students are expected to read assigned papers, search relevant literature and prepare scientific presentation on the paper. Students are expected to meet at least twice with their supervisors: once to clarify questions about the paper and to discuss an initial draft of their presentation, and once to discuss the full set of slides and improve the presentation.

Students signed up for the course who are unable to attend should contact us as soon as possible (email florian.zuleger@tuwien.ac.at).
Electronic versions of the papers will be provided to the students.

The presentations will tentatively take place during 16.6., 9:00-13:00.