Modul

Siehe Teilleistung.

Die Studierenden können Korrektheits-Eigenschaften von Software mittels verschiedener Logiken beschreiben. Sie kennen eine repräsentative Auswahl logischer Entscheidungsverfahren und können diese anwenden. Sie verstehen deren theoretische Grundlagen, praktische Eigenschaften und Grenzen und können diese für eigene Weiterentwicklungen einsetzen sowie deren Praxiseinsatz beurteilen.

Die Studierenden sind qualifiziert, zuverlässige Software-basierte Systeme zu entwickeln, die Qualität bestehender Systeme einzuschätzen und deren Qualität zu verbessern.

Die Studierenden sind qualifiziert, neue theoretische und praktische Verfahren, basierend auf den gelernten, zu entwickeln.

Siehe Teilleistung.

Entscheidungsverfahren sind Algorithmen, die für ein gegebenes Problem immer eine korrekte Ja/Nein-Antwort liefern.

Sie spielen in der Softwareverifikation eine entscheidende Rolle, da sich mit ihrer Hilfe eine Vielzahl von Korrektheitseigenschaften (z.B. in Bezug auf Speicherzugriffsfehler, Überläufe oder funktionale Eigenschaften) überprüfen und vollautomatisch beweisen lassen.

Die Vorlesung stellt eine Reihe von logischen Entscheidungsverfahren und ihre Anwendung in der automatischen Programmverifikation vor.

Themen sind unter anderem:

• SAT-Solving, DPLL
• DPLL(T)
• Gleichheit mit uninterpretierten Funktionen, Kongruenzabschluß
• Lineare Arithmetik ganzer Zahlen
• Bitvektoren und Machinenarithmetik
• Arrays
• Quantoren, Quantorenelimination
• Software Bounded Model Checking
• Symbolic Execution
• Predicate Abstraction
• Werkzeuge: LLBMC, KLEE, SatAbs

Der erfolgreiche Abschluss des Moduls Formale Systeme [M-INFO-100799] wird empfohlen.

2 SWS Vorlesung + 1 SWS Übungen

(Vor- und Nachbereitungszeiten: 4h/Woche für Vorlesung plus 2h/Woche für Übungen; Prüfungsvorbereitung: 15h)

Gesamtaufwand:
(2 SWS + 1 SWS + 4 SWS + 2 SWS) x 15h + 15h Prüfungsvorbereitung = 9x15h + 15h = 150h = 5 ECTS