Search

• < Previous
• 1
• Next >

---

Simulating reachability using first-order logic with applications to verification of linked data structures

Tal Lev-Ami ; Neil Immerman ; Thomas Reps ; Mooly Sagiv ; Siddharth Srivastava ; Greta Yorsh.

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the&nbsp;[&hellip;]

---

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

---