Module 8 — Compare BDD reachability with IC3 and PDR · Binary Decision Diagrams with CUDD

formal.org
Binary Decision Diagrams with CUDD

Module 8 — Compare BDD reachability with IC3 and PDRInvariants as unreachable bad states, CTL as fixpoints, IC3 and PDR in outline, a lab comparing BDD reachability with abc pdr, and where BDDs are used today.Katas in this module (4)

Kata 8.1 — Decide whether the invariant holds

Kata 8.2 — Name the engine that finishes

Kata 8.3 — Sum an ADD over its variables

Kata 8.4 — Find where BDDs are used today

Part of Binary Decision Diagrams with CUDD on formal.org.