Praktikum SAT/SMT-Solving
- type: Praktikum (P)
- semester: SS 2020
-
place:
Seminarraum 236, Geb. 50.34
-
time:
Di. 17:30 - 19:00
- lecturer: Prof. Dr. Carsten Sinz
- sws: 4
- lv-no.: 2400104
| Bemerkungen | 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. 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) |
| Literaturhinweise | Literatur wird in der Veranstaltung bekannt gegeben. |