Research Group Computer Science 2

Dept. of Computer Science

Seminar: Satisfiability Checking (S2, SS 2025)

Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, László Antal, Dr. Florian Frohn, Lina Gerlach, Jan-Christoph Kassing, József Kovács, Nils Lommen, Eleanore Meyer, Jasper Nalbach, Valentin Promies, Nicolai Radke

Contents

The focus of this seminar is automatic satisfiability checking of formulas. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulas or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification.

Prerequisites

• Participants should have knowledge in satisfiability checking and/or program verification or related areas (for example from courses on "Satisfiability Checking", "Modeling and Analysis of Hybrid Systems", "Logic Programming", "Functional Programming", "Term Rewriting", "Model Checking", "Static Program Analysis", "Semantics and Verification of Software", etc.)
• Interest in algorithmic aspects and practical applications of logical formalisms

Date

The seminar will take place as a block seminar in Summer 2025.

Area

Theoretical Computer Science

Further Details and Questions

For further details please contact Eleanore Meyer.

Research Group Computer Science 2

Dept. of Computer Science