Satisfiability Checking (SS 2016)

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

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", or "Term Rewriting")
Interest in algorithmic aspects and practical applications of logical formalisms

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.

Contacted your supervisor to obtain and discuss your literature until 23rd of May.
Until June 6th: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
Until July 4th: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
Until August 15th: Prepare your talk and send your slides to your supervisor.
Until August 22nd: Send an electronic version of your seminar paper to your supervisor such that it can be made available on the web page of the seminar.

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

Seminar: Satisfiability Checking