Mathematical Foundations of Model Checking

A 10-module graduate-level course on the mathematics behind model checking. Functions, fixed-point theory, Kripke structures, Büchi automata, and CTL — all grounded in formal verification practice.

Modules (10)

• Module 1 — Functions & Equivalence Relations — 3 katas
• Module 2 — Combinatorics & Counting
• Module 3 — Partial Orders & Lattices
• Module 4 — Monotone Functions & Fixed-Point Theory
• Module 5 — Well-Founded Relations & Ranking — 3 katas
• Module 6 — Composition & Product Construction — 3 katas
• Module 7 — Bisimulation & Equivalence
• Module 8 — ω-Automata, Büchi & Fairness — 3 katas
• Module 9 — Kripke Structures — 3 katas
• Module 10 — Computation Tree Logic — 3 katas

Every kata runs SymbiYosys in the browser: write the properties, run the proof, read the counterexample.