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.

翻译：我们报告了——据我们所知——首次关于（部分）有界内存安全性证明完整性阈值研究的中间结果。具体而言，我们考虑在不分配或释放内存的情况下遍历数组的堆操作程序。在此设定下，我们提出了程序验证中完整性阈值的首个概念，该概念将无界内存安全性证明简化为（部分）有界证明。此外，我们证明了对于简单类别的数组遍历程序，可以刻画其完整性阈值。最后，我们提出了在理论上（即扩展到更广泛的程序类别，如堆操作、树状数据结构）和通过强调自动化机会在实践上扩展该技术的研究方向。