Search

• < Previous
• 1
• Next >

Bounded Quantifier Instantiation for Checking Inductive Invariants

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