Home | english  | Impressum | Datenschutz | Sitemap | KIT

Praktikum SAT/SMT-Solving

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