Endowed professorship for reliable software systems in the automotive industry

Praktikum SAT/SMT-Solving

  • type: Praktikum (P)
  • semester: WS 19/20
  • time: 16.10.2019
    09:45 - 11:15 wöchentlich
    50.34 Raum 131
    50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
    weitere...

  • lecturer: Prof. Dr. Carsten Sinz
    Markus Iser
  • sws: 4
  • lv-no.: 2400104
Bemerkungen

SAT- und SMT-Solver sind wichtige Kernkomponenten in Entscheidungsverfahren der Logik. In diesem Praktikum sollen solche Solver neu entwickelt bzw. bestehende um aktuelle Verfahren erweitert werden.

Beschreibung

SAT-Solver sind universelle Problemlöser für kombinatorische Entscheidungsprobleme. SMT-Solver erweitern diese um sogenannte Theorien (wie z.B. Arithmetik) und finden unter anderem in der Programmverifikation Anwendung.

In diesem Praktikum sollen aktuelle Verfahren des SAT/SMT-Solvings in prototypischen Implementierungen umgesetzt und evaluiert werden.

Die konkreten Aufgabenstellungen wechseln und werden in einer Auftaktveranstaltung zu Beginn des Semesters bekanntgegeben.

Literaturhinweise

Literatur wird in der Veranstaltung bekannt gegeben.

Arbeitsbelastung

6 ECTS/LP:

15h Präsenzzeit

20h Literaturrecherche und Ausarbeitung der Aufgabenstellung

25h Erstellung und Halten der Abschlusspräsentation

120h Bearbeitung der Aufgabe (Implementation und Evaluierung)