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.

2022S, SE, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: SE Seminar
  • Format der Abhaltung: Distance Learning

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

- wissenschaftliche Publikationen zu lesen,
- sowohl Inhalt als auch Relevanz der Publikation zu verstehen,
- Literatursuche durchzuführen,
- wissenschaftliche Arbeiten zugänglich zu präsentieren.

Inhalt der Lehrveranstaltung

Das Seminar umfasst Themen im Bereich der Formalen Methoden. Es beschäftigt sich mit wegweisenden Ergebnissen und Publikationen in den Bereichen der Programmanalyse, des automatisierten Schließens und der computergestützten Verifikation. Jeder Studierende wählt eine wissenschaftliche Publikation aus einer vorgegebenen Liste und präesentiert dieses in einem halbstündigen Vortrag.

Methoden

Das vorrangige Ziel ist es, den Inhalt und die Relevanz der Publikation zu verstehen; falls notwendig, inhaltlich verwandte Publikationen zu lesen; und schlußendlich die Arbeit den anderen TeilnehmerInnen des Seminars zu präsentieren. Vor der Präsentation der Publikation müssen die Studierenden diese mit dem zugewiesenen Betreuer besprechen.

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: Leitfaden zum Umgang mit Plagiaten (PDF)

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mo.11:00 - 12:0014.03.2022 https://tuwien.zoom.us/j/95121006820 (LIVE)Vorbesprechung

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


PAPERS TO CHOOSE FROM:

Papers proposed and to be supervised by Katalin Fazekas:

Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno:
Finding Invariants of Distributed Systems: It's a Small (Enough) World After All
NSDI 2021
https://www.usenix.org/system/files/nsdi21-hance.pdf

Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel:
IC3 with Internal Signals
FMCAD 2021
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_14

Miguel Terra-Neves, Nuno Machado, Inês Lynce, Vasco M. Manquinho:
Concurrency Debugging with MaxSMT
AAAI 2019
https://doi.org/10.1609/aaai.v33i01.33011608

Aman Goel, Karem A. Sakallah:
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
NFM 2021
https://link.springer.com/chapter/10.1007/978-3-030-76384-8_9

Katalin Fazekas, Fahiem Bacchus, Armin Biere:
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
IJCAR 2018
https://link.springer.com/chapter/10.1007/978-3-319-94205-6_10

Papers proposed and to be supervised by George Kenison:

George Kenison, Richard Lipton, Joel Ouaknine, James Worrell:
On the Skolem Problem and Prime Powers
ISSAC 2020
https://dl.acm.org/doi/10.1145/3373207.3404036

Florian Luca, Joel Ouaknine, James Worrell:
Universal Skolem Sets
LICS 2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470513

Ezio Bartocci, Laura Kovacs, Miroslav Stankovic:
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
ATVA 2019
https://doi.org/10.1007/978-3-030-31784-3_15

Andreas Humenberger, Nikolaj Bjorner, Laura Kovacs:
Algebra-Based Loop Synthesis
IFM 2020
https://doi.org/10.1007/978-3-030-63461-2_24

Florian Frohn, Marcel Hark, Jurgen Giesl:
Termination of Polynomial Loops
SAS 2020
https://doi.org/10.1007/978-3-030-65474-0_5

ORGANISATION:

The topics and the organization of the seminar will be discussed during the initial meeting on Monday, March 14, 11:00 (in a Zoom meeting; link will be sent to all registered participants).

Students signed up for the course who are unable to attend should contact us as soon as possible.

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 to clarify questions about the paper and to discuss an initial draft of their presentation, and once to discuss the full set of slides and improve the presentation.

Students signed up for the course who are unable to attend should contact us as soon as possible (email george.kenison@tuwien.ac.at ).
Electronic versions of the papers will be provided to the students.

LVA-Anmeldung

Von Bis Abmeldung bis
21.02.2022 11:00 03.05.2022 23:59 03.06.2022 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Weitere Informationen

  • Anwesenheitspflicht!

Sprache

Englisch