Search

• < Previous
• 1
• Next >

---

Bounded Quantifier Instantiation for Checking Inductive Invariants

Yotam M. Y. Feldman ; Oded Padon ; Neil Immerman ; Mooly Sagiv ; Sharon Shoham.

We consider the problem of checking whether a proposed invariant $\varphi$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. While the problem is undecidable, modern SMT solvers can sometimes solve it automatically. However, they employ&nbsp;[&hellip;]

---

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

Makai Mann ; Ahmed Irfan ; Alberto Griggio ; Oded Padon ; Clark Barrett.

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;]

---