Completeness Thresholds for Memory Safety of Array Traversing Programs

Tobias Reinhard, Justus Fasse, Bart Jacobs

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 co…