Bounded Quantifier Instantiation for Checking Inductive Invariants

Yotam M. Y. Feldman, Oded Padon, Neil Immerman +2

We consider the problem of checking whether a proposed invariant $\phi$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. Whi…