Search

• < Previous
• 1
• Next >

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction&nbsp;[&hellip;]