Diese Seite auf Deutsch  Research Group Computer Science 2  Dept. of Computer Science RWTH

Seminar: Satisfiability Checking

(S2, WS 2009/2010)

LuFG Informatik II


Instructors

Prof. Dr. Erika Ábrahám, Prof. Dr. Jürgen Giesl, Xin Chen, Fabian Emmes, Carsten Fuhs, Nils Jansen, Ulrich Loup, Carsten Otto



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 2010. We have the following deadlines:



Requirements

Your seminar paper should have 10 - 15 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



Topics

DateTimeTopicSupervisorSpeaker
Feb 0810:00SMT for Non-Linear Interval ArithmeticX. Chen, U. LoupMarian Van de veire
Feb 0810:45Constraint Satisfaction ProblemsF. EmmesFlorian Corzilius
Feb 0811:30Electronic Design AutomationC. FuhsMaik Scheffler

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.

The slides of Prof. Ábrahám's presentation at the introductory meeting are available here.



Area

Theoretical Computer Science, Area of Specialization


Further Details and Questions

For further details please contact Carsten Fuhs.


Disclaimer  Research Group Computer Science 2  Dept. of Computer Science RWTH