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)