Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

Seminar SAT-Solving

  • Typ: Seminar
  • Semester: Hauptdiplom
  • Ort:

    Seminarraum -107 (50.34 UG)

  • Zeit:

    Mo 15:45-17:15

  • Beginn: 14.04.
  • Dozent:

    C. Sinz, H. Post

  • SWS: 2
  • LVNr.: 24827
  • Hinweis:

    Das Seminar wurde zusammengelegt mit dem Seminar "Formale Software-Entwicklung" von Prof. Schmitt.

Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie und Praxis eine herausragende Rolle. Es ist das erste als NP-vollständig erkannte Problem, und auch heute noch Ausgangspunkt vieler komplexitätstheoretischer
Untersuchungen. Darüber hinaus hat sich  SAT-Solving inzwischen als eines der wichtigsten grundlegenden Verfahren in der Verifikation von Hard- und Software
etabliert.

Im Seminar wollen wir historische und aktuelle Artikel rund um das SAT-Problem
betrachten zu Themen wie:
    •    Datenstrukturen und Algorithmen zum SAT-Solving
    •    Komplexität, handhabbare Unterklassen (tree-width, FPT)
    •    Effiziente Codierung kombinatorischer Probleme
    •    Visualisierung der Struktur von SAT-Problemen
    •    Querbeziehungen zur statistischen Physik
    •    Bounded Model Checking
    •    SAT-Solving in der Produkt-Konfiguration
    •    Software-Verifikation mittels SAT-Solvern
    •    SMT (Satisfiability Modulo Theory)

Organisatorisches

  • Vorträge können auf Englisch oder Deutsch gehalten werden.
  • Folien spätestens zwei Wochen vor Vortragstermin mit dem Betreuer durchsprechen.
  • Ausarbeitung: 10-15 Seiten, Abgabe zum Ende des Semesters
  • Vortragsdauer max. 40 Minuten plus 10 Minuten für Diskussion
  • Tipps zu Vortrag und Ausarbeitung: Seminarleitfaden von K. und N. Weicker
  • Vorträge am 09.07. finden im Seminarraum -109 statt.

Termine

14.04.2008: Vorbesprechung

05.05.2008: Einführung SAT-Solving (C. Sinz)

09.07.2008: Vorträge (max. 40min + 10min Diskussion)

14:00  Markus Iser: Visualisierung der Struktur von SAT-Instanzen mittels Graph-Layout
14:50  Simon Roth: Software Verifikation: Abstraction Refinement
15:40  Jan Rochel: Tree Decomposition für SAT