Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage
- Spezifizieren eines Systems an: Automaten, zeitliche Logik.- Algorithmen zur Verifizierung von Systemen verstehen: Model checking und abstrakte Interpretation.- Verwenden Constraint Solver (Erfüllbarkeitslöser) zum Erstellen von Model checkers
Modellierung von Hardware und Software, Überblick über computerunterstuetzte Verifikationsmethoden. Spezifikation durch Temporallogik und Automaten, Simulation und Bisimulation, Zustands-Explosion, explizite und symbolische Model Checking Verfahren, Abstraktion und Abstraktionsverfeinerung, Predicate Abstraction, Entscheidungsprozeduren, Beweisertools. Verifikationssoftware in der Praxis, šUberblick šuber Verifikation spezieller Systeme und aktuelle Entwicklungen.
Der Kurs besteht aus 8 Vorlesungen und 4 Übungsstunden, in denen die Schüler Beispiele aus Übungsblättern präsentieren.
Anmeldung über TISS Studierende der Kennzahlen 931,938 werden bevorzugt. Bitte LVA abonnieren. Hörsaalreservierungen sind für LVA 181.144 + 181.145.
ECTS Breakdown:----------------------------------25h Vorlesungen und Prüfung35h Prüfungsvorbereitung15h Übungsaufgaben----------------------------------75h (3 ECTS)----------------------------------
The course will have a final exam. The date and place of the final written exam will be announced later. Students are allowed to bring one A4-size sheet of hand-written notes to the exam. No other material is allowed.
aktuelle Infos bitte LVA abonnieren Ort: TISS
Bachelor in Informatik oder verwandten Gebieten
