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.

2022W, SE, 2.0h, 3.0EC
TUWEL

LVA-Bewertung

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

- 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, program analysis 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.

Proposed list of papers:

Papers proposed and to be supervised by Michael Rawson:

"AVATAR: The Architecture for First-Order Theorem Provers", Voronkov.
"Magic sets and other strange ways to implement logic programs", Bancilhon et al.
"Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning", Korovin.
"Translating Higher-Order Clauses to First-Order Clauses", Meng and Paulson.
"Reinforcement Learning of Theorem Proving", Kaliszyk et al.
"Finding Loop Invariants for Programs over Arrays Using a Theorem Prover", Kovács and Voronkov.
"Induction in Saturation-Based Proof Search", Reger and Voronkov.
"Twee: An Equational Theorem Prover", Smallbone.
"New Techniques in Clausal Form Generation", Reger, Suda and Voronkov.
"First Order Theorem Proving and Vampire", Kovács and Voronkov.



Papers proposed and to be supervised by Katalin Fazekas:

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors Using an SMT Theory of Sequences.
IJCAR 2022
https://doi.org/10.1007/978-3-031-10769-6_9

Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonás, Greg Kimberly:
Efficient SMT-Based Analysis of Failure Propagation.
CAV 2021
https://doi.org/10.1007/978-3-030-81688-9_10

Randy Hickey, Fahiem Bacchus:
Speeding Up Assumption-Based SAT.
SAT 2019
https://doi.org/10.1007/978-3-030-24258-9_11

William Schultz, Ian Dardik and Stavros Tripakis
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+
FMCAD 2022
https://doi.org/10.48550/arXiv.2205.06360

Ofer Guthmann, Ofer Strichman, Anna Trostanetski:
Minimal unsatisfiable core extraction for SMT.
FMCAD 2016
https://doi.org/10.1109/FMCAD.2016.7886661

Randal E. Bryant, Armin Biere, Marijn J. H. Heule:
Clausal Proofs for Pseudo-Boolean Reasoning.
TACAS 2022
https://doi.org/10.1007/978-3-030-99524-9_25

Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, João Marques-Silva:
Using MaxSAT for Efficient Explanations of Tree Ensembles.
AAAI 2022
https://ojs.aaai.org/index.php/AAAI/article/view/20292

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

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

Gilles Audemard, Laurent Simon:
Predicting Learnt Clauses Quality in Modern SAT Solvers.
IJCAI 2009
http://ijcai.org/Proceedings/09/Papers/074.pdf



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

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.17:00 - 18:0018.10.2022 https://tuwien.zoom.us/j/93425856420 (LIVE)Initial Meeting

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

ORGANISATION:

The topics and the organization of the seminar will be discussed during an initial meeting. (If you can not attend this initial meeting you should contact katalin.fazekas@tuwien.ac.at 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.

LVA-Anmeldung

Von Bis Abmeldung bis
31.08.2022 00:00 11.10.2022 23:59 18.10.2022 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Weitere Informationen

  • Anwesenheitspflicht!

Sprache

Englisch