181.221 Seminar Formal Methods
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2024S, SE, 2.0h, 3.0EC


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: SE Seminar
  • Format: Hybrid

Learning outcomes

After successful completion of the course, students are able to...

- read scientific papers,
- understand the content as well as the significance of a paper,
- literature research,
- present scientific work in an accessible manner

Subject of course

The seminar covers selected topics in the field of formal methods. The course revolves around seminal research papers in the fields of program analysis, 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. 


Proposed List of Papers

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,

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

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

Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel
Certified CNF Translations for Pseudo-Boolean Solving
SAT 2022
pp 16:1-16:25

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.

Teaching methods

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.

Mode of examination


Additional information


How to give a good talk (by Simon Peyton Jones, given in Vienna, October 2004):


(requires Real Player)

Please consider the plagiarism guidelines of TU Wien when writing your seminar paper: Directive concerning the handling of plagiarism (PDF)



Course dates

Wed10:00 - 11:0020.03.2024 https://tuwien.zoom.us/j/62245619828?pwd=dkVQTHJhYUJUQUZ6a0YxeGd5MFNYZz09Kickoff Meeting

Examination modalities

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)




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 daniela.kaufmann@tuwien.ac.at).
Electronic versions of the papers will be provided to the students.

Course registration

Begin End Deregistration end
19.02.2024 11:00 18.03.2024 23:59 18.03.2024 23:59


Study CodeObligationSemesterPrecon.Info
066 504 Master programme Embedded Systems Not specified
066 931 Logic and Computation Mandatory elective
066 937 Software Engineering & Internet Computing Mandatory elective


No lecture notes are available.


  • Attendance Required!