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

---

First-Order and Temporal Logics for Nested Words

Rajeev Alur ; Marcelo Arenas ; Pablo Barcelo ; Kousha Etessami ; Neil Immerman ; Leonid Libkin.

Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested&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;]

---

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

---