Reading of scientific papers,
literature research,
presentation of scientific work

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 papers. 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.

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: 

• David Damestani: "Efficiently Solving Quantified Bit-Vector Formulas"
• Pamina Georgiou: "Coming to Terms with Quantified Reasoning"
• Romana Jezek: "Sampling Invariants from Frequency Distributions"
• Stefan Stojanoski: "Triggerless Happy: Intermediate Verification with a First-Order Prover" 
• Deana Zafirova: "Relational Constraint Solving in SMT"

Final Paper Presentations - Schedule: 

• June 4, 2018, 8:00-11:00, Seminar room Menger (Favoritenstr. 9-11, 3rd floor)
• 8:00 -   9:00:  Deana Zafirova: "Relational Constraint Solving in SMT" 
• 9:00 - 10:00:  Romana Jezek: "Sampling Invariants from Frequency Distributions" 
• 10:00 - 11:00:  Pamina Georgiou: "Coming to Terms with Quantified Reasoning"

• June 14, 9:00-11:00, Seminar room Menger (Favoritenstr. 9-11, 3rd floor)
• 9:00 - 10:00:  David Damestani: "Efficiently Solving Quantified Bit-Vector Formulas" 
• 10:00 - 11:00:  Stefan Stojanoski: "Triggerless Happy: Intermediate Verification with a First-Order Prover" 

PAPERS to choose from - electronic versions of all papers is available [here]: 

• Automated Reasoning and Verification. 

1. Yuting Chen and Carlo A. Furia : "Triggerless Happy: Intermediate Verification with a First-Order Prover". IFM 2017: 295-311

2. Laura Kovacs, Simon Robillard, Andrei Voronkov: "Coming to Terms with Quantified Reasoning". POPL 2017: 260-270.

3. Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett. "Relational Constraint Solving in SMT". CADE 2017: 148-165. 

4. Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura:
"Efficiently Solving Quantified Bit-Vector Formulas". FMCAD 2010: 239-246.

• Invariant Generation and Verification.

5. Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodik: "Sampling Invariants from Frequency Distributions". FMCAD 2017: 100-107.

6. Zachary Kincaid, John Cyphert, Jason Breck, Thomas Reps. "Non-Linear Reasoning For Invariant Synthesis". POPL 2018: 54:1-54:33.

7. Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan: "Inductive Invariant Generation via Abductive Inference". OOPSLA 2013: 443-456.

8. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham: "Ivy: safety verification by interactive generalization". PLDI 2016: 614-630.

 

ORGANISATION:

The topics and the organization of the seminar will be discussed in an initial meeting on
Monday, March 19, 1 pm, 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 (email lkovacs@forsyte.at). 

Beachten Sie beim Verfassen der Ausarbeitung bitte die Richtlinie der TU Wien zum Umgang mit Plagiaten: https://www.tuwien.ac.at/fileadmin/t/ukanzlei/Lehre_-_Leitfaden_zum_Umgang_mit_Plagiaten.pdf

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

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

Slides of the Introductory lecture from March 19, 2018 are online.