Fundamentals of Model Checking

Formal verification is an effective method for ensuring correctness of computing systems deployed in a growing number of diverse safety critical domains across our society. This specialization introduces basic concepts and fundamentals of model checking, a critical approach to logic verification of computing systems including hardware, software, or both. Model checking, a branch of automated formal verification relying on rigorous mathematical methods, is often used to provide high confidence in the target systems. This specialization will first introduce modeling formalisms that are foundations for automated algorithmic analysis and show how different types of computing systems are represented in these formalisms. Second, it will introduce temporal logics and show how they can be used to precisely and unambiguously describe different properties to define correct requirements of target systems for model checking. Third, it will introduce basic graph-based model checking algorithms to decide the truth of the temporal logic properties against models of computing systems under verification. Third, it will introduce equivalence theories that can support methods of abstraction enabling model complexity reduction improving the efficiency of model checking. Finally, it will introduce the partial order reduction method that can substantially reduce the size of the state space produced by model checking for highly concurrent systems.