After successful completion of the course, students are able to...

- 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' paper assignment: 

Martin Exner: Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha. "egg: Fast and Extensible Equality Saturation". POPL 2021. https://doi.org/10.1145/3434304

Johannes Felzmann: Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel. "Fast Approximations of Quantifier Elimination". CAV 2023. https://doi.org/10.1007/978-3-031-37703-7_4

Henri Thölke:  Jakob Rath, Armin Biere, Laura Kovács.  "First-Order Subsumption via SAT Solving." FMCAD 2022. https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_22

Rasmus Rendal: Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli. "Reasoning About Vectors Using an SMT Theory of Sequences". IJCAR 2022. https://doi.org/10.1007/978-3-031-10769-6_9

Schedule of First Meeting on Paper/Presentation Discussion

Meeting place: Favoritenstrasse 9-11, Stiege 3, 3rd Floor, office HG0315 (office of Laura Kovács)

December 5, 12:00-13:00, Henri Thoelke
December 5, 15:00-16:00, Rasmus Kjaer

December 12, 12:00-13:00 Martin Exner
December 12, 13:00-14:00 Johannes Felzmann

 Schedule of Second Meeting on Seminar Talk: 

Meeting place: Favoritenstrasse 9-11, Stiege 3, 3rd Floor, office HG0315 (office of Laura Kovács)

January 16, 12:00-13:00 Henri Thoelke

January 16, 13:00-14:00 Johannes Felzmann

January 16, 15:00-16:00 Rasmus Kjaer

January 24, 15:00-16:00 Martin Exner

Schedule of Final Exam/FM Seminar Talks

Meeting place: Favoritenstrasse 9-11, Stiege 3, 3rd Floor, Menger Seminar room

January 30, 9:00-9:35 Henri Thoelke

January 30, 9:35-10:10 Martin Exner

January 30, 10:20-10:55 Johannes Felzmann

January 30, 10:55-11:30 Rasmus Kjaer

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 24, 2023. If you can not attend this initial meeting you should contact laura.kovacs@tuwien.ac.at. Slides of the kickoff are available at here. 

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 laura.kovacs@tuwien.ac.at. These preferences should be communicated via email, latest by November 6, 2023. 

Paper assignments will be announced and made online latest by November 9, 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:

• once during December 4-15, to clarify questions about the paper and to discuss an initial draft of their presentation,
• once during January 15-19, to discuss the full set of slides and improve the presentation. 

Final seminar presentations are planned during January 25-31, with exact dates TBD.