Satisfiability Checking (SS 2015)

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

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

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

If you haven't contacted your supervisor to obtain and discuss your literature yet, do so as soon as possible.
Until June 5th: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
Until June 24th: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
Until July 16th: Prepare your talk and send your slides to your supervisor.
Until July 27th: 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.

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

Seminar: Satisfiability Checking