Automatisches Beweisen - Grundlagen
Kenntnisse in den Grundlagen der mathematischen Logik, insbesondere hinsichtlich automatisierbaren Beweisverfahren und deren Anwendungen. Die Teilnehmer lernen exemplarisch die Grundlagen, Möglichkeiten und Grenzen von Logik-basierten Beweisverfahren in der Informatik kennen. Sie werden befähigt, moderne Verifikationsverfahren in der Industrie einzuführen und anzuwenden (z.B. Hardware- und Software-Verifikation, Konfiguration von Kraftfahrzeugen).
- Grundlagen: Terme und Induktion
- Aussagenlogik: Entscheidungsverfahren und Anwendungen (Resolution, SAT-Solving, BDD, Konfiguration von Kraftfahrzeugen)
- Prädikatenlogik: Beweisverfahren und Anwendungen (Resolution, Prolog)
- Spezielle Logiken: Beweisverfahren und Anwendungen (Hoare-Kalkül, Software-Verifikation)
Art | Vorlesung & Übung |
---|---|
Betreuer | Prof. Dr. Küchlin / Thore Kübart, M.Sc. Informatik |
Umfang | 2 SWS Vorlesung + 1 SWS Übung / 6 LP |
Termin | Vorlesung: Mi, 10 c.t. - 12 Uhr, wöchentlich |
Raum | Informatik/Kriminologie - Hörsaal A 301 |
Beginn | 13.04.2016 |
Klausur | Mi, 20.07.2016, 10-12, Morgenstelle, N 04 |
Campus Link | Link (Alle Veranstaltungsdetails) |
Übungsgruppe | Wochentag | Uhrzeit | Raum |
---|---|---|---|
Freitag | 10 c.t. - 12 Uhr | A301 |