  We report on intermediate results of -- to the best of our knowledge -- the
first study of completeness thresholds for (partially) bounded memory safety
proofs. Specifically, we consider heap-manipulating programs that iterate over
arrays without allocating or freeing memory. In this setting, we present the
first notion of completeness thresholds for program verification which reduce
unbounded memory safety proofs to (partially) bounded ones. Moreover, we
demonstrate that we can characterise completeness thresholds for simple classes
of array traversing programs. Finally, we suggest avenues of research to scale
this technique theoretically, i.e., to larger classes of programs (heap
manipulation, tree-like data structures), and practically by highlighting
automation opportunities.
