Module 8 — k-Induction & IC3/PDR

Unbounded verification via k-induction and IC3/PDR. Push inductive clauses forward through the transition relation and converge on an invariant that holds for all reachable states.

Katas in this module (3)

• Kata 8.1 — A k-Inductive Property
• Kata 8.2 — Non-Inductive Property Requires Strengthening
• Kata 8.3 — mode prove Runs These Algorithms

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