In this early preliminary report on an ongoing project, we present -- to the best of our knowledge -- the first study of completeness thresholds for memory safety proofs. Specifically we consider heap-manipulating programs that iterate over arrays without allocating or freeing memory. We present the first notion of completeness thresholds for program verification which reduce unbounded memory safety proofs to bounded ones. Moreover, we present some preliminary ideas on how completeness thresholds can be computed for concrete programs.

翻译：在本进行中项目的早期初步报告中，我们提出了——据我们所知——关于内存安全性证明的完备性阈值的首次研究。具体而言，我们考虑在未分配或释放内存的情况下遍历数组的堆操作程序。我们提出了程序验证中完备性阈值的首个概念，该概念将无界内存安全性证明简化为有界证明。此外，我们提出了一些关于如何为具体程序计算完备性阈值的初步思路。