Research Group Computer Science 2

Dept. of Computer Science

Seminar: Satisfiability Checking (S2, WS 2010/2011)

Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Carsten Fuhs, Nils Jansen, Ulrich Loup, Johanna Nellen, Carsten Otto, Thomas Ströder

Contents

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.

Times

The seminar will take place at the end of the lecture period in February 2011. We have the following deadlines:

• Nov 05: Contact your supervisor to obtain and discuss the literature
• Dec 02: Understand the content of your literature sources and discuss the conception of your paper with your supervisor
• Dec 20: Submit your complete seminar paper (10 pages incl. title and references)
• Feb 16: Bring sufficiently many copies of your corrected seminar paper to the seminar; you can make these copies at the research group

Requirements

Your seminar paper should have 10 pages and be written in either English or German. With this number of pages, there should not be any index or table of contents. Nevertheless, you should give a list of your references. If there are more than ten grammatical or spelling mistakes on a single page, the review of your paper will be aborted, and it will be returned to you immediately (please use an automated spell checker!).

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", "Term Rewriting", "Functional Programming", "Logic Programming", or "Mechanized Program Verification")
• Interest in algorithmic aspects and practical applications of logical formalisms

Topics

Date	Time	Topic	Supervisor	Speaker
Feb 16	10:00	Generalized DPLL	U. Loup	Devran Oelcer
Feb 16	10:45	DPLL(T) featuring Linear Real Arithmetic	J. Nellen	Felix Voigtländer
Feb 16	11:30	Quantified Boolean Formulae	N. Jansen	Paul Zakalek
Feb 16	12:15	SAT for Termination	C. Otto	Hanjie Zhao

The talks should not take more than 30 minutes and can be held in either English or German. The schedule for the talks is tentative.

Area

Theoretical Computer Science, Area of Specialization

Further Details and Questions

For further details please contact Thomas Ströder.

Disclaimer

Research Group Computer Science 2

Dept. of Computer Science