Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
Published in arxiv.org, 2023
Recommended citation: Tobias Reinhard. 2023. Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report. arXiv:2211.11885 https://arxiv.org/abs/2211.11885
[Bibtex]
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.
The paper corresponding to this technical report ( SOAP 2023 ) can be found here.