Module 3 — CEGAR & Predicate Abstraction

Counterexample-guided abstraction refinement: start coarse, test whether a counterexample is spurious, refine, and repeat until the proof closes.

Katas in this module (1)

• Kata 3.1 — Coarse Predicates Fail; Refine and Close

Part of Industrial Practice: Scaling Formal Verification on formal.org.