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.
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.
Papers proposed and to be supervised by Daniela Kaufmann
Daniela Kaufmann, Armin Biere and Manuel Kauers Verifying Large Multipliers by Combining SAT and Computer Algebra FMCAD 2019 pp 28-36, https://doi.org/10.23919/FMCAD.2019.8894250. Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli Bit-Precise Reasoning via Int-Blasting. VMCAI 2022 pp 496-518 https://doi.org/10.1007/978-3-030-94583-1_24 Marijn J.H. Heule, Manuel Kauers, Martina Seidl New ways to multiply 3 × 3-matrices, Journal of Symbolic Computation, Volume 104, 2021, pp 899-916 https://doi.org/10.1016/j.jsc.2020.10.003 Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel Certified CNF Translations for Pseudo-Boolean Solving SAT 2022 pp 16:1-16:25 https://doi.org/10.4230/LIPIcs.SAT.2022.16
Papers proposed and to be supervised by George Kenison
Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Mossbrugger, and Miroslav Stankovic"Solving Invariant Generation for Unsolvable Loops"Static Analysis 2022pp. 19--43https://doi.org/10.1007/978-3-031-22308-2_3
George Kenison, Richard Lipton, Joël Ouaknine, and James Worrell"On the Skolem Problem and Prime Powers"ISSAC 2020 pp. 289--296 https://doi.org/10.1145/3373207.3404036
Ashish Tiwari "Termination of Linear Programs" CAV 2004 pp. 70--82https://doi.org/10.1007/978-3-540-27813-9_6
Manuel Kauers and Veronika Pillwein"When Can We Detect That a P-Finite Sequence is Positive?"ISSAC 2010pp. 195–201https://doi.org/10.1145/1837934.1837974
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.
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)
Students will be graded based on:
1.) Ability to read and understand the papers assigned to them. Theeffort and initiative to independently read and understand the paperand to read up on related work will determine 50% of the grade. Thestudents' understanding of the paper will be evaluated during themeetings with the lecturer and by means of questions after the talk.
2.) Ability to present the material in an accessible way to their fellowstudents. The clarity and style of the presentation as well as thestudents' effort to prepare the talk (e.g., by designing their ownexamples rather than reusing material from the paper) determine 50% ofthe grade.
Additional information on grading: The relative difficulty of thepaper will be taken into account. Asking meaningful questions aboutthe presentations of fellow students will have a positive impacton 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)---------------------------------------
ORGANISATION:
The topics and the organization of the seminar will be discussed during the initial meeting on TBD (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.
