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.

翻译：在关于一个进行中项目的早期初步报告中,我们根据我们所知,提出了关于记忆安全证明完整性阈值的首次研究。具体地说,我们考虑了在不分配或释放内存的情况下对阵列循环的堆积操纵程序。我们提出了关于程序核查的完整性阈值的第一个概念,将无约束内存安全证明降低到约束性。此外,我们提出了一些关于如何计算具体程序的完整性阈值的初步想法。