Satisfiability Checking (SS 2019)

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

Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Stefan Dollase, Marcel Hark, Jera Hensel, Rebecca Haehn, Gereon Kremer,

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 August 1st, 2019 from 10 am to 1 pm in our seminar room (4201b). The preliminary discussion took place on April 4, 2019 at 10:30 in 5055.

Times

We have a series of strict deadlines before that.

Until April 19th: Contact your supervisor to obtain and discuss the literature.
Until April 25th: Possibility of withdrawing from the seminar without failing it.
Until May 17th: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
Until June 14th: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
Until July 18th: Prepare your talk and send your slides to your supervisor.
Until July 25th: Submit the final version of your seminar paper to your supervisor.

Requirements

Your seminar paper should have 10 pages in a format similar to the template given below. It can 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

Title	Literature	Supervisor	Student	Time
Verification of Neural Networks	Link	Prof. Dr. Erika Ábrahám	David Klüner	10:00-10:25
Termination of Triangular Integer Loops is Decidable	Link	Prof. Dr. Jürgen Giesl	Eric Skaliks	10:45-11:10
Proving termination of imperative programs using Max-SMT	Link	Stefan Dollase	Kai Liehr	11:30-11:55
Answer Set Programming Based on Propositional Satisfiability	Link	Jera Hensel	Dinh-An Ho	12:15-12:40

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

Disclaimer

Research Group Computer Science 2

Dept. of Computer Science

Seminar: Satisfiability Checking