Module 7 — Induction and Strengthening

formal.org
Discrete Mathematics for Formal Verification

Module 7 — Induction & StrengtheningBase case and inductive step as a solver sees them, BMC versus prove mode, why a true property may not be inductive, and how to strengthen an invariant until it closes.Katas in this module (6)

Kata 7.1 — Base Case and Inductive Step

Kata 7.2 — True but Not Inductive

Kata 7.3 — Strengthening the Invariant

Kata 7.4 — Clean Induction

Kata 7.5 — Strengthen the Induction

Kata 7.6 — Even Counter — Prove Mode

Part of Discrete Mathematics for Formal Verification on formal.org.