Making PROGRESS in Property Directed Reachability
summary
Implements Proof-Guided Restriction Skipping (PROGRESS) on top of PDR/IC3 to run model checking under arbitrary restrictions (fixing inputs/state bits to constants) and uses SAT queries with assumptions plus unsat cores to identify and retract only the restrictions that caused a spurious proof. Evaluated on HWMCC benchmarks, the prototype reuses clauses across restarts, excels at long error traces (depth ≥30), Proof-Guided Restriction Skipping (PROGRESS) doubles the amount of detected deep counterexamples and averages 5.65 restarts per solved restricted run.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:57Formal Safety Verification
- 1:37Abstraction
- 3:15Restrictions
- 5:15Progress
- 5:43Duel of Seekers
- 6:47Model Checking
- 7:24Why PDR
- 7:56How PDR works
- 9:09PDR time frames
- 9:40Proof obligations
- 11:52Proof of safety
- 13:07Proof of obligations
- 13:40Possible outcomes
- 16:44Retraction
- 17:26Implementation
- 19:45Results
- 22:00Observations
- 23:46Conclusion
- 24:51Questions