Completeness Thresholds for Memory Safety of Array Traversing Programs
Published in SOAP, 2023
Recommended citation: Tobias Reinhard, Justus Fasse and Bart Jacobs. 2023. Completeness Thresholds for Memory Safety of Array Traversing Programs. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis https://dl.acm.org/doi/abs/10.1145/3589250.3596143
[Bibtex]
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.
[Paper ACM / arXiv]
[Technical Report] (Full formalization and proofs.)
[Presentation]
Recommended citation for TR: Tobias Reinhard, Justus Fasse and Bart Jacobs. 2023. Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report. arXiv:2211.11885