Module 3 — Fixed-Point CTL Model Checking

CTL labeling via least and greatest fixed points. Implement EF, EU, EG, and AG queries as BDD fixed-point computations and verify correctness against RTL designs.

Katas in this module (1)

• Kata 3.1 — The Iteration Count IS the BMC Depth

Part of Decision Procedures for Hardware Formal Verification on formal.org.