We investigate the decidability of completely automatic program verification for programs that manipulate heaps, and in particular decision procedures for proving memory safety. The work in [Mathur et al. 2019a] identifies decidable sub-classes of uninterpreted programs, but does not address programs that can update functions, which are crucial to model heap-manipulating programs. We develop a new theory of programs, called alias-aware coherent programs, that admits decidable verification. We apply this theory to develop verification algorithms for memory safety— determining if a heap-manipulating program that allocates/frees memory locations and manipulates heap pointers does not dereference a memory location that is not allocated.

We consider this problem when the initial allocated heap forms a forest data-structure (i.e., a disjoint set of trees and lists). While the problem of checking memory safety of programs whose initial heap is a forest data-structure is undecidable, we identify a class of streaming-coherent programs for which the problem is decidable. Our experimental evaluation demonstrates that common library routines that manipulate forest data-structures using a single pass almost always fall in our decidable class. And show that our decision procedure for these programs is effective in both proving memory safety and in identifying memory safety errors.