Module 5 — Bounded Model Checking

BMC as SAT: unroll the transition relation k times, assert the negation of the property, and let the SAT solver find a counterexample or exhaust the search up to depth k.

Katas in this module (3)

• Kata 5.1 — Reach the Bug
• Kata 5.2 — Bug Depth versus BMC Depth
• Kata 5.3 — Sound But Not Complete

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