Fundamentals of Model Checking Specialization
Formal verification ensures the correctness of computing systems in safety-critical domains. This specialization introduces model checking, a mathematical approach to verifying hardware and software systems.
You’ll learn system modeling, temporal logic for defining requirements, and graph-based algorithms for verification, along with techniques like abstraction and partial order reduction to manage complexity.
Throughout this specialization, students will engage in a series of hands-on projects that connect theoretical foundations of system modeling and verification with practical implementation. Learners will progressively develop the ability to represent, analyze, and verify the behavior of complex systems through a combination of software construction, modeling, and algorithmic techniques.
In this specialization, you will learn how to:
- Obtain an overview of verification, position of model checking in the spectrum of verification approaches, pros and cons of model checking
- Describe modeling formalisms that are fundamental for automated model checking
- Understand temporal logics and how to use them to specify correctness requirements for computing systems under verification
- Understand the concept of partial order reduction and how it can improve the efficiency of model checking highly concurrent systems
Courses
- Introduction to Modeling for Formal Verification
- Temporal Logic Model Checking
- Equivalences, Abstraction, and Partial Order Reduction