Inhalt

[ 921COENMCHV21 ] VL (*)Model Checking

Versionsauswahl
Es ist eine neuere Version 2022W dieser LV im Curriculum Masterstudium Wirtschaftsinformatik 2023W vorhanden.
(*) Leider ist diese Information in Deutsch nicht verfügbar.
Workload Ausbildungslevel Studienfachbereich VerantwortlicheR Semesterstunden Anbietende Uni
3 ECTS M1 - Master 1. Jahr Informatik Martina Seidl 2 SSt Johannes Kepler Universität Linz
Detailinformationen
Quellcurriculum Masterstudium Computer Science 2021S
Ziele (*)The students understand the fundamental concepts of explicit and symbolic model checking techniques and know how to apply them for verification tasks. They are familiar with the algorithmic aspects of explicit model checking and are able to implement basic model checking approaches.
Lehrinhalte (*)formal models in computer science, finite state machines, equivalence checking, conformance checking, predicate abstraction, (bi-)simulation, automata minimization, explicit vs. symbolic representation of systems, reachability analysis, optimizing search with hashing, partial order reduction, liveness and fairness, combinatorial logic, AIGs, BDDs.
Beurteilungskriterien (*)Exam plus practical projects (together with exercise class).
Lehrmethoden (*)Slide-based presentation, tool demos, practical exercises.
Abhaltungssprache Englisch
Literatur (*)Slides. Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem editors, Springer 2018.
Lehrinhalte wechselnd? Nein
Sonstige Informationen (*)http://fmv.jku.at/mc
Äquivalenzen (*)in collaboration with 921COENMCHK21: UE Model Checking (1.5 ECTS) equivalent to
921COENMCHK13: KV Model Checking (4.5 ECTS)
Präsenzlehrveranstaltung
Teilungsziffer -
Zuteilungsverfahren Direktzuteilung