Towards Decision Procedures for Programs Handling Pointers

often to reason about the set of memory cells that are reachable from
an initial memory cell. To automatize this kind of reasoning, we
introduce and prove decidable two languages involving sets and
reachability. The first language extends a basic fragment of set
theory with a second-order theory of reachability. The second
language extends the basic fragment with a first-order approximation
of the theory of reachability. While the first language better
captures the notion of reachability, the second one has the advantage
to allow for a more efficient decision procedure.

(joint work with Silvio Ranise)