Software Model-Checking as Cyclic-Proof Search
summary
Claims that many software model-checking procedures are just proof-search strategies for a cyclic proof system and gives a worked mapping: symbolic execution plus SMT checks, Craig interpolation for cuts, and model-based projection for counterexample classification. Reconstructs PDR/IC3-style routines, proves soundness as a corollary, and derives a repetition-complete variant of PDR that terminates by grouping infinite counterexample traces. Highlights the heuristic maximal conservativity and an unexpected link to an efficient game solver.
AI-written summary · about
chapters (9)
- 0:00Software model-checking intro
- 4:18Software model checking background
- 13:16Connecting model checking to cyclic-proof
- 16:27Symbolic execution as proof rule
- 21:48Cut rule and predicate abstraction
- 22:54Lazy abstraction with interpolation
- 25:28PDR reconstruction
- 26:12Model checking as cyclic-proof strategies
- 27:01Q&A