Seminar: Satisfiability checking

The focus of this seminar is on fully automated satisfiability checking of logical formulas. We consider several logics, e.g., pure propositional logic, bit-vector arithmetic, floating-point arithmetic, or real and integer arithmetic. We will discuss algorithms and techniques for efficient satisfiability checking as well as practical applications.

Prerequisites
Participants should be interested in algorithmic aspects of theoretical computer science, and should possess basic knowledge in the area of formal methods (for example from courses on “Satisfiability Checking”, “Modeling and Analysis of Hybrid Systems”, “Model Checking”, “Logic Programming”, “Functional Programming”, “Term Rewriting” etc.).

Requirements
You will work out a written document (seminar paper) and give a presentation about a scientific topic. The seminar paper should have 10 pages and be written in either English or German. You do not need to provide an index or table of contents, but attach a list of references. You can find templates for your paper here.
The presentations will be given in either English or German, use slides and should have a duration of 25 minutes.

Dates
The seminar will take place as a block seminar at the end of the semester.
04.11.2016 Contact your supervisor to obtain and discuss relevant literature.
18.11.2016 Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
09.12.2016 Complete your seminar paper (10 pages including title and references, English or German) and send it to your supervisor to get comments for improvements. Please use a spell checker!
23.12.2016 Send the final version of your seminar paper (pdf) to your supervisor such that it can be made available on the seminar’s web page.
20.01.2017 Prepare your talk and send your slides to your supervisor to get comments for improvements.
03.02.2017 Send the final version of your slides (pdf) to your supervisor such that it can be made available on the seminar’s web page.
TBA Presentation

Topics

  • Preprocessing techniques for SAT or LRA
  • Theory combination with the Nelson-Oppen integration scheme
  • Computing unsatisfiable cores
  • Model construction during SAT solving
  • Solving nonlinear equalities with virtual substitution
  • Using SMT for bounded model checking

Material

Contact
For further details please contact Gereon Kremer.