Completeness Thresholds for Memory Safety of Array Traversing Programs

Explore a 19-minute video presentation from the SOAP 2023 conference that delves into the study of completeness thresholds for partially bounded memory safety proofs. Learn about the first notion of completeness thresholds for program verification that reduce unbounded memory safety proofs to partially bounded ones, specifically for heap-manipulating programs iterating over arrays without memory allocation or deallocation. Discover how researchers characterize completeness thresholds for simple classes of array traversing programs and consider potential avenues for scaling this technique to larger program classes and practical automation opportunities. Gain insights into program verification, bounded proofs, model checking, and separation logic as presented by researchers from KU Leuven, Belgium.

[SOAP'23] Completeness Thresholds for Memory Safety of Array Traversing Programs