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 field of automated reasoning, program analysis 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.

Students can select from the following research papers: 

André Duarte, Konstantin Korovin:
Ground Joinability and Connectedness in the Superposition Calculus. IJCAR 2022: 169-187
https://link.springer.com/chapter/10.1007/978-3-031-10769-6_11

Uwe Waldmann:
On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus. IJCAR (1) 2024: 244-261
https://link.springer.com/chapter/10.1007/978-3-031-63498-7_15

Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik:
Monitoring Algorithmic Fairness. CAV 2023: 358-382
https://link.springer.com/chapter/10.1007/978-3-031-37703-7_17

Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields.CAV 2024: 3-25
https://link.springer.com/chapter/10.1007/978-3-031-65627-9_1

Charlie Murphy, Zachary Kincaid:
Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement. CAV 2024: 89-109
https://link.springer.com/chapter/10.1007/978-3-031-65627-9_5

Chenglin Wang, Fangzhen Lin:
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches. CAV 2024: 409-430
https://link.springer.com/chapter/10.1007/978-3-031-65627-9_20

Anders Miltner, Ziteng Wang, Swarat Chaudhuri, Isil Dillig:
Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata. CAV 2024: 41-63
https://link.springer.com/chapter/10.1007/978-3-031-65633-0_3

Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, R. Venkatesh, Grigory Fedyukovich:
Weakest Precondition Inference for Non-Deterministic Linear Array Programs. TACAS 2024: 175-195
https://link.springer.com/chapter/10.1007/978-3-031-57249-4_9

Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler:
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains. TACAS 2024: 237-257
https://link.springer.com/chapter/10.1007/978-3-031-57249-4_12

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

ORGANISATION:

The topics and the organization of the seminar will be discussed during the initial meeting on October 10, 2024. If you can not attend this initial meeting you should contact laura.kovacs@tuwien.ac.at.  

From the list of proposed research papers, students should select two papers that they would prefer presenting. Only one paper needs to be presented by one student. Students should email their respective Top 2 papers to the seminar organizers. These preferences should be communicated via email, latest by October 21, 2024. 

Paper assignments will be announced and made online latest by October 23 4, 2023. 

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:

Final seminar presentations are planned during January 2025, exact date TBD.