Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

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.