Research Group Computer Science 2

Dept. of Computer Science

Seminar: Satisfiability Checking (S2, SS 2021)

Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Ahmed Abiba, Rebecca Haehn, Marcel Hark, Dominik Meier, Fabian Meyer, Jasper Nalbach, Dr. Stefan Schupp

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

Area

Theoretical Computer Science

Further Details and Questions

For further details please contact Dominik Meier.

Research Group Computer Science 2

Dept. of Computer Science