| 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) |
Praktikum SAT/SMT-Solving
| Typ: | Praktikum (P) | ||
|---|---|---|---|
| Semester: | WS 19/20 | ||
| Zeit: | 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 |
||
| Dozent: | Prof. Dr. Carsten Sinz Markus Iser |
||
| SWS: | 4 | ||
| LVNr.: | 2400104 | ||
