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

Satisfiability Checking

(S2, SS 2019)

LuFG Informatik II


Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Stefan Dollase, Marcel Hark, Jera Hensel, Rebecca Haehn, Gereon Kremer,


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 (e.g., in July 2019). The preliminary discussion took place on April 4, 2019 at 10:30 in 5055.


The seminar will take place on the as a block seminar on August 1st 2019. We have a series of strict deadlines before that.


Your seminar paper should have 10 pages in a format similar to the template given below. It can 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!


Linear Optimization via SMTLinkRebecca HaehnDennis Prudlik
Verification of Neural NetworksLinkProf. Dr. Erika ÁbrahámDavid Klüner
Termination of Triangular Integer Loops is DecidableN.N.Prof. Dr. Jürgen GieslEric Skaliks
Proving termination of imperative programs using Max-SMTLinkStefan DollaseKai Liehr
Answer Set Programming Based on Propositional SatisfiabilityLinkJera HenselDinh-An Ho

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 Marcel Hark.

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