Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)

TL;DR

This paper introduces the concept of completeness thresholds to extend bounded proofs for memory safety to unbounded guarantees, demonstrated through a bubble sort example.

Contribution

It presents a novel approach to derive unbounded guarantees from bounded proofs using completeness thresholds, enhancing proof robustness.

Findings

Bounded proofs can be extended to unbounded guarantees using completeness thresholds.

A bubble sort implementation example illustrates the practical application of the approach.

Few specific inputs are sufficient for bounded proofs to ensure unbounded guarantees.

Abstract

Bounded proofs are convenient to use due to the high degree of automation that exhaustive checking affords. However, they fall short of providing the robust assurances offered by unbounded proofs. We sketch how completeness thresholds serve as a bridge, allowing us to derive unbounded guarantees from bounded proofs. Using a bubble sort implementation as example, we demonstrate that a bounded proof only needs to consider a few specific inputs to yield unbounded guarantees.