[Poster Presentation] Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
Date:
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. Completeness thresholds serve as a bridge, allowing us to derive unbounded guarantees from bounded proofs. With this poster we present the first notion of completeness thresholds that is applicable to program verification. Specifically, we target memory safety proofs.
[Poster on Zenodo]