Home | deutsch  | Legals | Data Protection | Sitemap | KIT

Entscheidungsverfahren mit Anwendungen in der Softwareverifikation

Entscheidungsverfahren mit Anwendungen in der Softwareverifikation
type:
semester: WS 18/19
time: 16.10.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


17.10.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

23.10.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

24.10.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

30.10.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

31.10.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

06.11.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

07.11.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

13.11.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

14.11.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

20.11.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

21.11.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

27.11.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

28.11.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

04.12.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

05.12.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

11.12.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

12.12.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

18.12.2018
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

19.12.2018
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

08.01.2019
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

09.01.2019
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

15.01.2019
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

16.01.2019
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

22.01.2019
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

23.01.2019
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

29.01.2019
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

30.01.2019
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

05.02.2019
11:30 - 13:00 wöchentlich
50.34 Raum 236
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten

06.02.2019
15:45 - 17:15 wöchentlich
50.34 Raum 301
50.34 INFORMATIK, Kollegiengebäude am Fasanengarten


lecturer: Markus Iser
Prof. Dr. Carsten Sinz
sws: 3
lv-no.: 2400073
Beschreibung

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
Arbeitsbelastung

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