Achtung ! Wegen eines Fehlers wird derzeit der Studienbeitragsstatus und somit auch der Fortmeldungsstatus falsch angezeigt. An der Behebung des Fehlers wird gearbeitet. Wir danken für Ihr Verständnis!

181.221 Seminar Formale Methoden
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2019W, SE, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: SE Seminar

Lernergebnisse

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

Inhalt der Lehrveranstaltung

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 paper. The students are expected to read and understand the paper and prepare and present a half-hour talk on the topic. 

PAPER ASSIGNMENT:

  • Thomas Hader, supervised by Laura Kovacs:

Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98

  • Mathias Hofer, supervised by Pavol Cerny: 

Bas Ketsman, Aws Albarghouthi and Paraschos Koutris: Distribution Policies for Datalog. ICDT 18 Database Theory: 17:1-17:22

  • Samuel Pilz, supervised by Florian Zuleger: 

Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey: A true positives theorem for a static race detector. PACMPL 3(POPL) 2019: 57:1-57:29.

  • Hannes Siebenhandl, supervised by Pavol Cerny: 

Kartik Nagar and Suresh Jagannathan: Automated Parameterized Verification of CRDTs. CAV 2019: 459-477.

  • Michael Strassersupervised by Florian Zuleger:

Mnacho Echenim, Radu Iosif, Nicolas Peltier: The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS 2019: 242-259

 

Proposed list of papers: 

Papers proposed and to be supervised by Laura Kovacs: 

  • Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli: A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98
  • Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett: Datatypes with Shared Selectors. IJCAR 2018: 591-608
  • Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar and Aarti Gupta: Quantified Invariants via Syntax-Guided-Synthesis. CAV 2019: 259-277.
  • Aws Albarghouthi, Loris D'Antoni and Samuel Drews: Efficient Synthesis with Probabilistic Constraints. CAV 2019: 278-296.
  • Greg Anderson, Shankara Pailoor, Isil Dillig, Swarat Chaudhuri: Optimization and Abstraction: a Synergistic Approach for Analyzing Neural Network Robustness. PLDI 2019: 731-744

Papers proposed and to be supervised by Florian Zuleger

  • Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham: Reducing liveness to safety in first-order logic. PACMPL 2(POPL) 2018: 26:1-26:33 
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier: The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS 2019: 242-259
  • Jérôme Leroux, Sylvain Schmitz: Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. LICS 2019: 1-13 
  • Christian Müller, Helmut Seidl, Eugen Zalinescu: Inductive Invariants for Noninterference in Multi-agent Workflows. CSF 2018: 247-261
  • Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey: A true positives theorem for a static race detector. PACMPL 3(POPL) 2019: 57:1-57:29 

Papers proposed and to be supervised by Pavol Cerny

  • M Arashloo, Y Koral, M Greenberg, J Rexford, D Walker: SNAP: Stateful network-wide abstractions for SIGCOMM 2016: 29-43
  • Ilya Sergey, James R. Wilcox, and Zachary Tatlock, Programming and Proving with Distributed Protocols POPL 2018: 28:1-28:30
  • Bas Ketsman, Aws Albarghouthi and Paraschos Koutris: Distribution Policies for Datalog. ICDT 18 Database Theory: 17:1-17:22
  • K. Mamouras, M. Raghothaman, R. Alur, Z. Ives, and S. Khanna. StreamQRE: Modular specification and Efficient Evaluation of Quantitative Queries over Streaming Data. PLDI 2017: 693-708
  • Kartik Nagar and Suresh Jagannathan: Automated Parameterized Verification of CRDTs. CAV 2019: 459-477.

Methoden

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.

Prüfungsmodus

Prüfungsimmanent

Weitere Informationen

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)


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

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.10:00 - 10:4516.10.2019 Seminar room Menger, Favoritenstrasse 9-11, 3rd floorFM Seminar - Introduction, Organization
Mo.09:00 - 12:3016.12.2019 Seminar room Menger, Favoritenstrasse 9-11, 3rd floorStudent presentations

Leistungsnachweis

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


SCHEDULE: 

  • October 16, 10-10:45am: Introductory seminar, Menger room
  • October 16-November 12: Individual meetings between students and seminar responsibles
  • November 11-15: Student presentations

ORGANISATION:

The topics and the organization of the seminar will be discussed after an initial meeting on October 16, 10-10:45amin the Menger meeting room (Favoritenstrasse 9, 3rd floor).

Students signed up for the seminar who are unable to attend this initial meeting should contact us as soon as possible (email laura.kovacs@tuwien.ac.at).

Students are expected to read assigned papers, search relevant literature and prepare scientific presentation on the paper.  

Student are expected two have at least two individual meetings with seminar lecturers (the lecturer responsible to supervise the chosen paper), discussing the content of the paper and its presentation.

Student presentations  will take place during 11-15 November, 2019 (exact date/time to be decided).

LVA-Anmeldung

Von Bis Abmeldung bis
04.09.2019 00:00 22.10.2019 23:59 22.10.2019 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Weitere Informationen

  • Anwesenheitspflicht!

Sprache

Englisch