Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report

TL;DR

This paper introduces the concept of completeness thresholds for verifying memory safety in array-traversing heap programs, enabling reduction of unbounded proofs to bounded ones, with initial ideas for computing these thresholds.

Contribution

It proposes the first notion of completeness thresholds for memory safety proofs and explores initial methods for their computation in array-manipulating programs.

Findings

First formalization of completeness thresholds for memory safety

Reduction of unbounded proofs to bounded verification tasks

Initial approaches to compute thresholds for concrete programs

Abstract

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.