Es ist eine neuere Version 2025W dieser LV im Curriculum Masterstudium Wirtschaftsinformatik 2025W vorhanden.
(*) Leider ist diese Information in Deutsch nicht verfügbar.
Workload
Ausbildungslevel
Studienfachbereich
VerantwortlicheR
Semesterstunden
Anbietende Uni
1,5 ECTS
M1 - Master 1. Jahr
Informatik
Martina Seidl
1 SSt
Johannes Kepler Universität Linz
Detailinformationen
Quellcurriculum
Masterstudium Computer Science 2022W
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
(*)Same as corresponding lecture:
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 lecture).
Lehrmethoden
(*)Student projects.
Abhaltungssprache
Englisch
Literatur
(*)Slides.
Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem editors, Springer 2018.
