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

---

Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words

Philipp Weis ; Neil Immerman.

It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of&nbsp;[&hellip;]

---