Software Model-Checking as Cyclic-Proof Search
summary
Claims that many software model-checking algorithms are exactly proof-search strategies for a cyclic proof system, so a single logical framework reconstructs PDR, Impact and k-step unwindings, supplies soundness proofs for free, and exposes when SMT-based interpolation and cut formulas succeed or fail. The paper formalizes weakest-precondition (greatest fixpoint) reasoning, shows how SE-derived rules plus forward criterion and interpolants recover PDR-style invariants, and ties maximal-conservativity heuristics to an efficient solver for games over infinite graphs.
AI-written summary · about