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
Please consider the plagiarism guidelines of TU Wien when writing your seminar paper:
http://www.tuwien.ac.at/fileadmin/t/ukanzlei/t-ukanzlei-english/Plagiarism.pdfPlease consider the plagiarism guidelines of TU Wien when writing your seminar paper:
Directive concerning the handling of plagiarism (PDF)Please consider the plagiarism guidelines of TU Wien when writing your seminar paper:
Directive concerning the handling of plagiarism (PDF)