Office of Academic Affairs
Indian Institute of Science Education and Research Bhopal

Electrical Engineering and Computer Science

ECS 415: Probabilistic Model Checking (4)

Learning Objectives:

Formal verification is the process of checking whether a design satisfies some requirements (properties). Model checking is the most popular method for automatic formal verification of safety critical software and hardware systems. It can be used to assess both qualitative and quantitative properties of complex systems. This course focuses on the fundamentals of model checking for probabilistic/stochastic models. These models are typically used to capture the behavior of systems that are subject to uncertainties, e.g., randomized distributed algorithms, queuing systems, economics, dynamic power management in embedded systems and systems biology. 

We will discuss model checking algorithms for several probabilistic models and present equivalence relations for comparing the behavior of these probabilistic models.

Course Contents:

Selected Readings:

Papers:


Previous Back to Course List Next