703048 VU SAT/SMT Solving

Sommersemester 2019 | Stand: 11.06.2019 LV auf Merkliste setzen
703048
VU SAT/SMT Solving
VU 2
5
keine Angabe
keine Angabe
Englisch

Absolventinnen und Absolventen dieses Moduls erkennen Probleme, in denen SAT- und SMT-Solver sinnvoll einsetzbar sind, verstehen die grundlegende Funktionsweise dieser Werkzeuge und können sie auch in eigenen Programmen erfolgreich verwenden.

Wie kann die Korrektheit von sicherheitskritischer Soft- und Hardware sichergestellt werden? Wie kann eine Fluglinie die Arbeitszeit ihrer Crew so auf Flüge verteilen, dass Kosten minimiert, Regulierungen eingehalten werden, und Kapazitätspuffer bestehen? Wie kann eine begrenzte Menge an Tests fuer ein Softwaresystem möglichst viele Situationen abdecken?
Für Verifikations-, Optimierungs- und Planungsprobleme wie diese erwies sich SAT/SMT in den letzten 15 Jahren als Katalysator, mit dem bislang kaum effizient bearbeitbare Probleme praktisch lösbar wurden. Was steckt dahinter?

Die automatische Analyse von Hardware- und Softwaresystemen erfordert die effiziente Bearbeitung von grossen und komplexen Systemen. Leistungsfähige Solver für das aussagenlogische Erfüllbarkeitsproblem (SAT-Solver) spielen dabei schon seit Beginn der 2000er Jahre eine herausragende Rolle. Sie bearbeiten effizient das NP-harte Erfuellungsproblem in der Aussagenlogik, und viele Problemstellungen können darauf reduziert werden. In der Praxis werden diese aber meist abstrakter modelliert, und die Übersetzung in ein aussagenlogisches Problem kann aufwändig sein. SMT (Satisfiability Modulo Theories) erweitert die reine Aussagenlogik (SAT) um Theorien wie Arithmetik, Bitvektoren und uninterpretierte Funktionen. SMT-Solver kombinieren so die Effizienz der SAT-Solver mit der Mächtigkeit einer ausdrucksstarken Logik. Der IBM HVC-Award bezeichnet SMT daher als den größten Fortschritt in der automatischen Verifikation der letzten Jahre.

Diese Lehrveranstaltung behandelt die SAT und SMT zugrundeliegenden Problemstellungen, theoretische Grundlagen von entsprechenden Solvern und betrachtet exemplarisch einige Anwendungsfälle.
Konkrete Inhalte sind:
SAT- und SMT-Probleme, DPLL und DPLL(T), Optimierungen, spezifische Lösungsverfahren für ausgewählte Theorien (Simplex, Fourier-Motzkin)

Im Rahmen von Vorträgen wird theoretisches Wissen vermittelt, das mit Hilfe von theoretischen Aufgaben und kleinen Programmierprojekten zur Anwendung gebracht und vertieft wird.

Lehrveranstaltungsimmanent durch regelmässige Aufgabenstellungen, zusätzlich schriftliche Tests

Diese Lehrveranstaltung kann als Wahlmodul verwendet werden.

Siehe dazu auch https://www.uibk.ac.at/informatik/studium/anerkennung (Zuordnungsbestätigung)

siehe Termine
Gruppe 0
Datum Uhrzeit Ort
Fr 08.03.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 15.03.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 22.03.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 29.03.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 05.04.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 12.04.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 03.05.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 10.05.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 17.05.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 24.05.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 07.06.2019
12.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Fr 14.06.2019
13.15 - 16.00 HSB 9 HSB 9 Barrierefrei
Fr 21.06.2019
13.15 - 15.00 HSB 9 HSB 9 Barrierefrei
Mo 01.07.2019
14.15 - 16.00 HSB 9 HSB 9 Barrierefrei Prüfung