LFU:online

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