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.

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.

Literatur wird in der Veranstaltung bekannt gegeben.

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)