course: Fortgeschrittene Themen des Model Checking

number:
150521
teaching methods:
seminar
media:
Moodle
responsible person:
Prof. Dr. Thomas Zeume
lecturer:
Prof. Dr. Thomas Zeume (Mathematik)
language:
german
HWS:
2
CP:
3
offered in:
summer term

dates in summer term

  • seminar: according to agreement

Exam

Die Angaben zu den Prüfungsmodalitäten (im WiSe 2020/2021 | SoSe 2021) erfolgen vorbehaltlich der aktuellen Situation. Notwendige Änderungen aufgrund universitärer Vorgaben werden zeitnah bekanntgegeben.
Form of exam:seminar
Registration for exam:Directly with the lecturer
continual assessment

goals

In der Veranstaltung Model Checking haben wir die theoretischen Grundlagen des Model Checkings kennen gelernt. Insbesondere haben wir die Spezifikationssprachen LTL und CTL eingeführt, ihre Ausdrucksstärke untersucht, und die wichtigsten algorithmischen Ansätze für das Model Checking erarbeitet.

content

Wie kann die Korrektheit von Software und Hardware formal überprüft werden? Im Model Checking werden Software- und Hardware-Module durch Transitionssysteme formalisiert; gewünschte Eigenschaften mit Hilfe logischer Formalismen formal beschrieben; und mit Hilfe von Algorithmen automatisiert überprüft, ob ein Transitionssystem eine formal spezifizierte Eigenschaft besitzt.

In diesem Seminar wollen wir uns mit weiterführenden, aktuellen Themen im Bereich Model Checking beschäftigen.

requirements

Keine

recommended knowledge

Veranstaltung "Model Checking"

miscellaneous

InteressentInnen melden sich beim Dozenten unter: thomas.zeume@rub.de