Research Group Computer Science 2  Dept. of Computer Science RWTH

Seminar:
Satisfiability Checking

(S2, SS 2015)

LuFG Informatik II


Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Cornelius Aschermann, Florian Corzilius, Florian Frohn, Jera Hensel, Gereon Kremer, Johanna Nellen, Stefan Schupp, Thomas Ströder


Contents

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


Prerequisites


Date

The seminar will take place on the 30th and 31st of July 2015 in our seminar room (4201b). We have a series of strict deadlines before that.


Initial Meeting

The initial meeting will take place on the 30th of April, 4pm, in our seminar room (4201b).


Requirements

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!


Topics

Date Time Student Supervisor Topic
30.07.15 09:30 Todorov, Georgi Prof. Dr. Jürgen Giesl Introduction to SAT and SMT via the DPLL Algorithm
10:15 Hans, Christian Gereon Kremer Incremental SAT
11:00 Neuberger, Lukas Stefan Schupp Interval Constraint Propagation
11:45 Hütter, Dustin Gereon Kremer and Stefan Schupp SMT-NIA via SMT-LIA
Lunch
13:15 Müller, Norman Florian Corzilius Nonlinear Real Arithmetic via Sum of Squares
14:00 Casatchina, Elena Prof. Dr. Erika Ábrahám and Florian Corzilius Quantified Boolean Formulas
14:45 Haps, Kim Prof. Dr. Erika Ábrahám Bitvectors
31.07.15 09:30 Hermanns, Judith Jera Hensel Program Analysis via Constraint Solving
10:15 Neuss, Malte Prof. Dr. Jürgen Giesl Termination Analysis via MAX-SAT
11:00 Pago, Benedikt Thomas Ströder Nontermination Analysis via Symbolic Execution and SMT
11:45 Karaca, Bugra Thomas Ströder Synthesizing shortest XOR circuits using SAT

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


Templates

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


SVN

If you want to use subversion for your paper and / or slides, please contact Gereon Kremer.


Further Details and Questions

For further details please contact Florian Frohn.

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