Model Checking#

Model checking is a formal verification technique for automatically checking whether a system satisfies a given specification.

Topics#

• Buchi Automata
• Linear Temporal Logic
• Bisimulation
• Computation Tree Logic
• Bisimulation-Quotienting Algorithms
• Simulation-Quotienting Algorithms
• Stutter Bisimulation
• Stutter Linear-Time Relations
• Partial Order Reduction
• Timed Automata
• Probabilistic Computational Tree Logic
• Probabilistic Bisimulation

Resources#

Books#

• Principles of Model Checking by Christel Baier, Joost-Pieter Katoen
• Model Checking by Edmund M. Clarke, Orna Grumberg, Doron A. Peled
• Model Checking and Abstract Interpretation by Patrick Cousot

Online Resources#

• MIT: Model Checking
• Stanford: Model Checking
• CMU: Model Checking

Practice Problems#

• Model Checking Exercises
• Model Checking Problems
• Model Checking Challenges