Satisfiability Checking (SS 2017)

Seminar:
Satisfiability Checking
(S2, SS 2017)
LuFG Informatik II

Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Florian Frohn, David Korzeniewski, Jera Hensel, 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 will take place as a block seminar on the 24th of July 2017 from 9 am to 4 pm in our seminar room (4201b). We have a series of strict deadlines before that.

Contacted your supervisor to obtain and discuss your literature until 12th of May.
Until June 2nd: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
Until June 23rd: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
Until July 14th: Prepare your talk and send your slides to your supervisor.
Until July 20th: 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 2nd of May 2017, 12:00, 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
24.07.17	9:00	Idil Esen Zulfikar	Prof. Dr. Erika Ábrahám	Minimal Infeasible Subset
	9:45	Nicolas Jezuita	Jera Hensel	Answer Set Programming
	10:30	Moritz Clever	Gereon Kremer	Difference Logic
	11:15	Joel Charles	Gereon Kremer	Nelson Oppen Integration Scheme
	13:00	Ömer Sali	Johanna Nellen	Interval Constraint Propagation
	13:45	Mohammad Touhidur Rahman	Prof. Dr. Jürgen Giesl	SMT for Termination of LLVM
	14:30	Marta Grobelna	Florian Frohn	Termination Analysis via MAX-SMT
	15:15	Fabian Böller	David Korzeniewski	Compositional Safety via MAX-SMT

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

Disclaimer

Research Group Computer Science 2

Dept. of Computer Science

Seminar: Satisfiability Checking