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

Seminar:
Satisfiability Checking

(S2, SS 2016)

LuFG Informatik II


Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Florian Corzilius, Florian Frohn, David Korzeniewski, Gereon Kremer, Johanna Nellen, 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


Date

The seminar takes place on the 25th (E3, room 9u09) and 26th (E3, room 9222) of August 2016. We have a series of strict deadlines before that.


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
25.08.16 09:30 Böhr, Nico David Korzeniewski Introduction to SAT and SMT via the DPLL Algorithm
10:15 Sabau, Alex Gereon Kremer Symmetry Breaking
11:00 Gerasimov, Arkadii Gereon Kremer Nelson Oppen Integration Scheme
11:45 Ilov, Petyo Prof. Dr. Erika Ábrahám Omega-Test
13:15 Srecec, Stefan Stefan Schupp SMT-NIA via SMT-LIA
14:00 Winkler, Tobias Florian Corzilius Polyhedral Approximation of NRA
26.08.16 09:30 Nehring-Wirxel, Julius Florian Frohn Synthesis of Polynomial Interpretations
10:15 Kruse, Sebastian Prof. Dr. Jürgen Giesl SMT for Termination of LLVM
11:00 Frerich, Kai Prof. Dr. Jürgen Giesl Termination Analysis via MAX-SMT
11:45 Penners, Ralf David Korzeniewski Compositional Safety via MAX-SMT
13:15 Sanka, Klea Prof. Dr. Erika Ábrahám Bounded Model Checking
14:00 Kraeutmann, David Florian Frohn Integration of SMT to Coq

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.


Further Details and Questions

For further details please contact Florian Frohn.

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