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) |