Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

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)