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
23.10.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
30.10.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
06.11.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
13.11.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
20.11.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
27.11.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
04.12.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
11.12.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
18.12.2019
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
08.01.2020
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
15.01.2020
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
22.01.2020
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
29.01.2020
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
05.02.2020
09:45 - 11:15 wöchentlich
50.34 Raum 131
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten
-
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) |