Hauptseminar: Satisfiability Modulo Theories (SMT, WiSe 2025/26)

Recognized as "Hauptseminar Theoretische Informatik" and "Seminar für Masterstudierende". For BSc students, participation is possible after consultation with the instructor.

Overview

Satisfiability Modulo Theories (SMT) extends propositional satisfiability (SAT) by adding background theories such as arithmetic, arrays, or bit-vectors. SMT solvers combine efficient SAT-solving technology with theory reasoning and are today among the most powerful automated reasoning tools.

In this seminar, students will study and present selected research papers in the area of SMT. Each participant will give a presentation and prepare a written summary of their topic.

Organization

  • Weekly seminar meetings (2 hours)
  • Instructor: Lydia Kondylidou
  • Language: English (presentations may be given in German or English)

Place and Time

ActivityTimePlaceStartEnd
SeminarThu 10–12 c.t.Oettingenstr. 67, room U12716.10.202505.02.2026

Requirements and Grading

  • Active participation in discussions
  • One 30-minute presentation (including Q&A)
  • Written report (8–12 pages) on the assigned topic
  • Grading will be based on presentation (50%) and report (50%)

Schedule

A detailed schedule with topics and paper assignments will be announced after the preliminary meeting. The preliminary meeting takes place on Thu, 16.10.2025, 10:00, Oettingenstr. 67, room U127.

Material

All seminar materials (papers, slides, and further references) will be provided here as the course progresses.

In addition, please register on Moodle using the registration key: SMT2526.

Chat

A Zulip chat stream will be set up for organizational questions and discussions:

Zulip-Server: https://chat.ifi.lmu.de/#narrow/channel/475-TCS-25W26-SMT Stream: TCS-25W26-SMT

News

To top