论文标题
阵列遍历程序的记忆安全性的完整性阈值：早期技术报告
Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
论文作者
论文摘要
在这项关于正在进行的项目的早期技术报告中，我们介绍了 - 据我们所知，首次研究完整性阈值以进行记忆安全性证明。具体而言，我们考虑堆积的程序，这些程序在不分配或释放内存的情况下迭代阵列。我们提出了第一个用于程序验证的完整性阈值的概念，该概念将无限的内存安全证明减少到有限的记忆安全证明。此外，我们提出了一些有关如何计算具体程序的完整性阈值的初步想法。
In this early technical 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.
