Model Checking
3 ECTS
Aim:This course is an introduction to model checking, an automatic verification technique of concurrent and reactive systems. In the first part of the course we study the kripke structure as a model of reactive concurrent systems, then we introduce the linear and branching time temporal logics and model checking algorithms for these logics. Finally we describe how to represent
Content:
- Reactive Systems Modeling
- Temporal Logics (CTL, LTL, CTL*)
- Model Checking Algorithms
- Binary Decision Diagram
- Symbolic Model Checking