Diese Seite auf Deutsch  Research Group Computer Science 2  Dept. of Computer Science RWTH

Satisfiability Checking

(S2, SS 2017)

LuFG Informatik II


Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Florian Frohn, David Korzeniewski, Jera Hensel, Gereon Kremer, Johanna Nellen, Stefan Schupp


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.



The seminar will take place as a block seminar on the 24th of July 2017 from 9 am to 4 pm in our seminar room (4201b). We have a series of strict deadlines before that.

Initial Meeting

The initial meeting will take place on the 2nd of May 2017, 12:00, in our seminar room (4201b).


Your seminar paper should have 10 pages and be written in either English or German. Do not provide an index or table of contents, but attach a list of references. More than 5 spelling or grammar mistakes on a single page will lead to an immediate rejection of your paper, so please use an automated spell checker!


Date Time Student Supervisor Topic
24.07.17 9:00 Idil Esen Zulfikar Prof. Dr. Erika Ábrahám Minimal Infeasible Subset
9:45 Nicolas Jezuita Jera Hensel Answer Set Programming
10:30 Moritz Clever Gereon Kremer Difference Logic
11:15 Joel Charles Gereon Kremer Nelson Oppen Integration Scheme
13:00 Ömer Sali Johanna Nellen Interval Constraint Propagation
13:45 Mohammad Touhidur Rahman Prof. Dr. Jürgen Giesl SMT for Termination of LLVM
14:30 Marta Grobelna Florian Frohn Termination Analysis via MAX-SMT
15:15 Fabian Böller David Korzeniewski Compositional Safety via MAX-SMT

The talks should not take more than 25 minutes and can be held in either English or German.


You can find templates for your paper here. Using them is optional.

Further Details and Questions

For further details please contact David Korzeniewski.

Disclaimer  Research Group Computer Science 2  Dept. of Computer Science RWTH